================================= Developer Guide ================================= Building GPUVerify ================== The GPUVerify toolchain is a pipeline that uses different components. This guide will walk you through the build process. There are specific instructions for Linux, Mac OS X and Windows however they have a common set of prerequisites which are: * CMake >=2.8.12 * Python 2.7 * Git * Subversion Basic Prequisites ----------------- GPUVerify requires python >= 2.7 and the python module `psutil `_. On Windows, we recommend installing psutil from a `prebuilt binary `_. On Linux/OSX, we recommend installing psutil with pip:: $ pip install psutil Linux and Mac OS X ------------------ In addition to the common prerequisites Linux and Mac OS X builds of GPUVerify require GCC >= 4.7 or Clang >= 3.1 and a recent version of Mono since part of the toolchain uses C#. You should use a version of Mono >= 3.4.0. To build GPUVerify follow this guide in a bash shell. Note ``${BUILD_ROOT}`` refers to where ever you wish to build GPUVerify. Replace as appropriate or setup an environment variable.:: $ export BUILD_ROOT=/path/to/build .. Note Sphinx is incredibly picky about indentation in lists. Everything in the list must be indented aligned with first letter of list text. Code blocks must start and end with a blank line and code blocks must be further indented from the list text. #. Obtain Mono from ``_ and install. #. Get the LLVM and Clang sources (note that GPUVerify depends on LLVM 3.8):: $ export LLVM_RELEASE=38 $ mkdir -p ${BUILD_ROOT}/llvm_and_clang $ cd ${BUILD_ROOT}/llvm_and_clang $ svn co http://llvm.org/svn/llvm-project/llvm/branches/release_${LLVM_RELEASE} src $ cd ${BUILD_ROOT}/llvm_and_clang/src/tools $ svn co http://llvm.org/svn/llvm-project/cfe/branches/release_${LLVM_RELEASE} clang Configure LLVM and Clang for building (we do an out of source build):: $ mkdir -p ${BUILD_ROOT}/llvm_and_clang/build $ cd ${BUILD_ROOT}/llvm_and_clang/build $ cmake -D CMAKE_BUILD_TYPE=Release -D LLVM_TARGETS_TO_BUILD=NVPTX ../src Compile LLVM and Clang:: $ make -jN where ``N`` is the number of jobs to run in parallel. #. Get libclc and build:: $ mkdir -p ${BUILD_ROOT}/libclc $ cd ${BUILD_ROOT}/libclc $ svn co http://llvm.org/svn/llvm-project/libclc/trunk -r260301 src $ cd ${BUILD_ROOT}/libclc/src $ ./configure.py --with-llvm-config=${BUILD_ROOT}/llvm_and_clang/build/bin/llvm-config \ --with-cxx-compiler=c++ \ --prefix=${BUILD_ROOT}/libclc/install \ nvptx-- nvptx64-- $ make $ make install #. Get Bugle and configure for building (we do an out of source build):: $ cd ${BUILD_ROOT} $ git clone https://github.com/mc-imperial/bugle.git ${BUILD_ROOT}/bugle/src $ mkdir ${BUILD_ROOT}/bugle/build $ cd ${BUILD_ROOT}/bugle/build $ cmake -D LLVM_CONFIG_EXECUTABLE=${BUILD_ROOT}/llvm_and_clang/build/bin/llvm-config \ -D CMAKE_BUILD_TYPE=Release \ -D LIBCLC_DIR=${BUILD_ROOT}/libclc/install \ ../src Compile Bugle:: $ make -jN where ``N`` is the number of jobs to run in parallel. #. Get the Z3 SMT Solver and build:: $ export Z3_RELEASE=z3-4.4.1 $ cd ${BUILD_ROOT} $ git clone https://github.com/Z3Prover/z3.git $ git checkout -b ${Z3_RELEASE} ${Z3_RELEASE} $ cd ${BUILD_ROOT}/z3 $ python scripts/mk_make.py $ cd build $ make -jN where ``N`` is the number of jobs to run in parallel. Make a symbolic link; ``GPUVerify.py`` looks for ``z3.exe`` not ``z3`` :: $ ln -s z3 z3.exe #. (Optional) Get the CVC4 SMT Solver and build. Note that building CVC4 further requires automake and boost:: $ cd ${BUILD_ROOT} $ git clone https://github.com/CVC4/CVC4.git ${BUILD_ROOT}/CVC4/src $ cd ${BUILD_ROOT}/CVC4/src $ MACHINE_TYPE="x86_64" contrib/get-antlr-3.4 $ ./autogen.sh $ export ANTLR=${BUILD_ROOT}/CVC4/src/antlr-3.4/bin/antlr3 $ ./configure --with-antlr-dir=${BUILD_ROOT}/CVC4/src/antlr-3.4 \ --prefix=${BUILD_ROOT}/CVC4/install \ --best --enable-gpl \ --without-glpk --without-abc \ --disable-shared --enable-static $ make $ make install Make a symbolic link; ``GPUVerify.py`` looks for ``cvc4.exe`` not ``cvc4`` :: $ cd ${BUILD_ROOT}/CVC4/install/bin $ ln -s cvc4 cvc4.exe #. Get GPUVerify code and build C# components:: $ cd ${BUILD_ROOT} $ git clone https://github.com/mc-imperial/gpuverify.git $ cd ${BUILD_ROOT}/gpuverify $ xbuild /p:Configuration=Release GPUVerify.sln #. Configure GPUVerify front end. GPUVerify uses a front end python script (GPUVerify.py). This script needs to be aware of the location of all its dependencies. We currently do this by having an additional python script (gvfindtools.py) with hard coded absolute paths that a developer must configure by hand. gvfindtools.py is ignored by Mercurial so each developer can have their own configuration without interfering with other users. :: $ cd ${BUILD_ROOT}/gpuverify $ cp gvfindtools.templates/gvfindtools.dev.py gvfindtools.py Open gvfindtools.py in a text editor and edit the paths. If you followed this guide strictly then these paths will be as follows and you should only need to change the ``rootDir`` variable. :: rootDir = "${BUILD_ROOT}" #< CHANGE THIS PATH # The path to the Bugle Source directory. # The include-blang/ folder should be there bugleSrcDir = rootDir + "/bugle/src" # The Path to the directory where the "bugle" executable can be found. bugleBinDir = rootDir + "/bugle/build" # The path to the libclc Source directory. libclcSrcDir = rootDir + "/libclc/src" # The path to the libclc install directory. # The include/ and lib/clc/ folders should be there libclcInstallDir = rootDir + "/libclc/install" # The path to the llvm Source directory. llvmSrcDir = rootDir + "/llvm_and_clang/src" # The path to the directory containing the llvm binaries. # llvm-nm, clang and opt should be there llvmBinDir = rootDir + "/llvm_and_clang/build/bin" # The path containing the llvm libraries llvmLibDir = rootDir + "/llvm_and_clang/build/lib" # The path to the directory containing the GPUVerify binaries. # GPUVerifyVCGen.exe, GPUVerifyCruncher.exe and GPUVerifyBoogieDriver.exe should be there gpuVerifyBinDir = rootDir + "/gpuverify/Binaries" # The path to the z3 Source directory. z3SrcDir = rootDir + "/z3" # The path to the directory containing z3.exe z3BinDir = rootDir + "/z3/build" # The path to the cvc4 Source directory. cvc4SrcDir = rootDir + "/CVC4/src" # The path to the directory containing cvc4.exe cvc4BinDir = rootDir + "/CVC4/install/bin" #. (Optional) Build the documentation. This requires the Sphinx python module, which you can install using ``pip``.:: $ pip install Sphinx $ cd ${BUILD_ROOT}/gpuverify/Documentation $ make html #. Run the GPUVerify test suite. :: $ cd ${BUILD_ROOT}/gpuverify $ ./gvtester.py --write-pickle run.pickle testsuite To run the GPUVerify test suite using the CVC4 SMT Solver: :: $ ./gvtester.py --gvopt="--solver=cvc4" --write-pickle run.pickle testsuite You can also check that your test run matches the current baseline. :: $ ./gvtester.py --compare-pickle testsuite/baseline.pickle run.pickle You should expect the last line of output to be.:: INFO:testsuite/baseline.pickle = new.pickle This means that your install passes the regression suite. Windows ------- In addition to the common prerequisites a Windows build of GPUVerify requires Microsoft Visual Studio 2012 or later. To build GPUVerify follow this guide in a powershell window. Note ``${BUILD_ROOT}`` refers to where ever you wish to build GPUVerify. Replace as appropriate or setup an environment variable.:: > ${BUILD_ROOT}='C:\path\to\build' We recommend that you build GPUVerify to a local hard drive like ``C:`` since this avoids problems with invoking scripts on network mounted drives. #. (Optional) Setup Microsoft Visual Studio tools for your shell. This will enable you to build projects from the command line.:: pushd 'C:\Program Files (x86)\Microsoft Visual Studio 12.0\VC' cmd /c "vcvarsall.bat & set" | foreach { if ($_ -match "=") { $v = $_.split("="); set-item -force -path "ENV:\$($v[0])" -value "$($v[1])" } } popd You can add this permanently to your ``$Profile`` so that the Microsoft compiler is always available at the command-line. In case you have Visual Studio 2015, replace ``Microsoft Visual Studio 12.0`` by ``Microsoft Visual Studio 14.0``. #. Get the LLVM and Clang sources (note that GPUVerify depends LLVM 3.8):: > $LLVM_RELEASE=38 > mkdir ${BUILD_ROOT}\llvm_and_clang > cd ${BUILD_ROOT}\llvm_and_clang > svn co http://llvm.org/svn/llvm-project/llvm/branches/release_$LLVM_RELEASE src > cd ${BUILD_ROOT}\llvm_and_clang\src\tools > svn co http://llvm.org/svn/llvm-project/cfe/branches/release_$LLVM_RELEASE clang Configure LLVM and Clang for building (we do an out of source build):: > mkdir ${BUILD_ROOT}\llvm_and_clang\build > cd ${BUILD_ROOT}\llvm_and_clang\build > cmake -G "Visual Studio 12" ` -D LLVM_TARGETS_TO_BUILD="X86;NVPTX" ` ..\src In case you have Visual Studio 2015, replace ``Visual Studio 12`` by ``Visual Studio 14``. This may require a version of CMake later than 2.8.8. Compile LLVM and Clang. You can do this by opening ``LLVM.sln`` in Visual Studio and building, or alternatively, if you have setup the Microsoft tools for the command line, then:: > msbuild /m /p:Configuration=Release LLVM.sln #. Get libclc source and binaries. You can download the binaries from the GPUVerify website and unzip this in ``${BUILD_ROOT}``. From the command line do:: > mkdir ${BUILD_ROOT}\libclc > cd ${BUILD_ROOT}\libclc > svn co http://llvm.org/svn/llvm-project/libclc/trunk -r260301 src > cd ${BUILD_ROOT} > $libclc_url = "http://multicore.doc.ic.ac.uk/tools/downloads/libclc-nightly.zip" > (new-object System.Net.WebClient).DownloadFile($libclc_url, "${BUILD_ROOT}\libclc-nightly.zip") > $shell = new-object -com shell.application > $zip = $shell.namespace("${BUILD_ROOT}\libclc-nightly.zip") > $dest = $shell.namespace("${BUILD_ROOT}") > $dest.Copyhere($zip.items(), 0x14) > del ${BUILD_ROOT}\libclc-nightly.zip #. Get Bugle and configure for building (we do an out of source build):: > cd ${BUILD_ROOT} > mkdir ${BUILD_ROOT}\bugle > git clone https://github.com/mc-imperial/bugle.git ${BUILD_ROOT}\bugle\src > mkdir ${BUILD_ROOT}\bugle\build > cd ${BUILD_ROOT}\bugle\build > $LLVM_SRC = "${BUILD_ROOT}\llvm_and_clang\src" > $LLVM_BUILD = "${BUILD_ROOT}\llvm_and_clang\build" > cmake -G "Visual Studio 12" ` -D LLVM_SRC=$LLVM_SRC ` -D LLVM_BUILD=$LLVM_BUILD ` -D LLVM_BUILD_TYPE=Release ` -D LIBCLC_DIR=${BUILD_ROOT}\libclc\install ` ..\src In case you have Visual Studio 2015, replace ``Visual Studio 12`` by ``Visual Studio 14``. This may require a version of CMake later than 2.8.8. Compile Bugle. You can do this by opening ``Bugle.sln`` in Visual Studio and building, or alternatively, if you have setup the Microsoft tools for the command line, then:: > msbuild /m /p:Configuration=Release Bugle.sln #. Get the Z3 SMT Solver and build:: > $Z3_RELEASE="z3-4.4.1" > cd ${BUILD_ROOT} > git clone https://github.com/Z3Prover/z3.git > cd ${BUILD_ROOT}\z3 > git checkout -b $Z3_RELEASE $Z3_RELEASE > python scripts\mk_make.py > cd build > nmake #. (Optional) Get the CVC4 SMT Solver:: > cd ${BUILD_ROOT} > mkdir -p ${BUILD_ROOT}\cvc4\build > cd ${BUILD_ROOT}\cvc4\build > $cvc4_url = "http://cvc4.cs.nyu.edu/builds/win32-opt/unstable/cvc4-2016-03-26-win32-opt.exe" > (new-object System.Net.WebClient).DownloadFile($cvc4_url, "${BUILD_ROOT}\cvc4\build\cvc4.exe") #. Get GPUVerify code and build. You can do this by opening ``GPUVerify.sln`` in Visual Studio and building, or alternatively, if you have setup the Microsoft tools for the command line, then:: > cd ${BUILD_ROOT} > git clone https://github.com/mc-imperial/gpuverify.git > cd ${BUILD_ROOT}\gpuverify > msbuild /p:Configuration=Release GPUVerify.sln #. Configure GPUVerify front end:: > cd ${BUILD_ROOT}\gpuverify > copy gvfindtools.templates\gvfindtools.dev.py gvfindtools.py Open gvfindtools.py in a text editor and edit the paths. If you followed this guide strictly then these paths will be as follows and you should only need to change the ``rootDir`` variable. :: rootDir = r"${BUILD_ROOT}" #< CHANGE THIS PATH # The path to the Bugle Source directory. # The include-blang/ folder should be there bugleSrcDir = rootDir + r"\bugle\src" # The Path to the directory where the "bugle" executable can be found. bugleBinDir = rootDir + r"\bugle\build\Release" # The path to the libclc Source directory. libclcSrcDir = rootDir + r"\libclc\src" # The path to the libclc install directory. # The include/ and lib/clc/ folders should be there libclcInstallDir = rootDir + r"\libclc\install" # The path to the llvm Source directory. llvmSrcDir = rootDir + r"\llvm_and_clang\src" # The path to the directory containing the llvm binaries. # llvm-nm, clang and opt should be there llvmBinDir = rootDir + r"\llvm_and_clang\build\Release\bin" # The path containing the llvm libraries llvmLibDir = rootDir + r"\llvm_and_clang\build\Release\lib" # The path to the directory containing the GPUVerify binaries. # GPUVerifyVCGen.exe, GPUVerifyCruncher.exe and GPUVerifyBoogieDriver.exe should be there gpuVerifyBinDir = rootDir + r"\gpuverify\Binaries" # The path to the z3 Source directory. z3SrcDir = rootDir + r"\z3" # The path to the directory containing z3.exe z3BinDir = rootDir + r"\z3\build" # The path to the directory containing cvc4.exe cvc4BinDir = rootDir + r"\cvc4\build" #. (Optional) Build the documentation. This requires the Sphinx python module, which you can install using ``pip``.:: $ pip install Sphinx $ cd ${BUILD_ROOT}\gpuverify\Documentation $ make html #. Run the GPUVerify test suite. :: $ cd ${BUILD_ROOT}\gpuverify $ .\gvtester.py --write-pickle run.pickle testsuite To run the GPUVerify test suite using the CVC4 SMT Solver: :: $ .\gvtester.py --gvopt="--solver=cvc4" --write-pickle run.pickle testsuite You can also check that your test run matches the current baseline. :: $ .\gvtester.py --compare-pickle testsuite\baseline.pickle run.pickle You should expect the last line of output to be:: INFO:testsuite/baseline.pickle = new.pickle This means that your install passes the regression suite. Deploying GPUVerify =================== To deploy a stand alone version of GPUVerify run:: $ mkdir -p /path/to/deploy/gpuverify $ cd ${BUILD_ROOT}/gpuverify $ ./deploy.py /path/to/deploy/gpuverify In the case you only built the Z3 solver, additionally supply the ``--solver=z3`` option to ``deploy.py``. This will copy the necessary files to run a standalone copy of GPUVerify in an intelligent manner by - Reading ``gvfindtools.py`` to figure out where the dependencies live. - Reading ``gvfindtools.templates/gvfindtoolsdeploy.py`` to determine the directory structure inside the deploy folder. - Copying ``gvfindtools.templates/gvfindtoolsdeploy.py`` into the deploy folder as ``gvfindtools.py`` for ``GPUVerify.py`` to use. No additional modification of any files is required provided you have correctly configured your development folder. Building Boogie =============== The GPUVerify repository has a pre-built version of Boogie inside it to make building the project a little bit easier. If you wish to rebuild Boogie for use in GPUVerify then follow the steps below for Linux and Mac OS X.:: $ cd ${BUILD_ROOT} $ git clone https://github.com/boogie-org/boogie.git $ cd boogie/Source $ xbuild /p:TargetFrameworkProfile="" /p:Configuration=Release Boogie.sln $ cd ../Binaries $ ls ${BUILD_ROOT}/gpuverify/BoogieBinaries \ | xargs -I{} -t cp {} ${BUILD_ROOT}/gpuverify/BoogieBinaries Test framework ============== GPUVerify uses a python script ``gvtester.py`` to instrument the GPUVerify.py front-end script with a series of tests. These tests are located in the folder ``testsuite/`` with each test being contained in a seperate folder. Test file syntax ---------------- Each test is a file named ``kernel.cu`` or ``kernel.cl`` (for CUDA and OpenCL respectively). These files contain special comments at the head of the file that instruct ``gvtester.py`` what to do. The syntax is as follows:: ::= "//" ( "pass" | ("xfail:" ) ) ::= "COMMAND_LINE_ERROR" | "CLANG_ERROR" | "OPT_ERROR" | "BUGLE_ERROR" | "GPUVERIFYVCGEN_ERROR" | "NOT_ALL_VERIFIED" ::= "//" ? ::= | " "+ ::= "//" ```` is telling ``gvtester.py`` whether or not the kernel is expected to pass ("pass") or expected to fail ("xfail"). If the kernel is expected to fail then ```` is the expected return code (as a string) from ``GPUVerify.py``. Note for the most current list of values that ```` can take run:: $ ./gvtester.py --list-xfail-codes ```` is telling ``gvtester.py`` what command line arguments to pass to ``GPUVerify.py``. ```` is a single ``GPUVerify.py`` command line argument. Each command line argument must be seperated by one or more spaces. Note as stated in the Backus-Naur form it is legal to pass no command line arguments. The path to the kernel for ``GPUVerify.py`` is implicitly passed as the last command line argument to ``GPUVerify.py`` so it should **not** be stated in ````. Special substitution variables can be used inside ```` which will expand as follows: - ``${KERNEL_DIR}`` : The absolute path to the directory containing the kernel without a trailing slash. ```` is telling ``gvtester.py`` what regular expression to match against the output of ``GPUVerify.py`` if ``GPUVerify.py``'s return code is not as expected. ```` is any Python regular expression supported by the ``re`` module. ```` can be repeated on mulitiple lines. Note that every character after ``//`` until the end of the line is interpreted as the regular expression so it is wise to avoid trailing spaces. Here is a more concrete example .. code-block:: c++ //xfail:COMMAND_LINE_ERROR //--bad-command-option --boogie-file=${KERNEL_DIR}/axioms.bpl //--bad-command-option not recognized\. //GPUVerify:[ ]+error:[ ]* //GPUVerify: Try --help for list of options //This is not a regex because we left a line that did not begin with "//" __kernel void hello(__global int* A) { //... } Pickle format ------------- ``gvtester.py`` is capable of storing information about executed tests in the "Pickle" format. Use the ``--write-pickle`` option to write a pickle file after running the tests. This file can be examined using the ``--read-pickle`` option and the ``--compare-pickles`` option. Baseline -------- A pickle file ``testsuite/baseline.pickle`` is provided which should record ``gvtester.py`` being run on ``testsuite`` in the repository. It is intended to be a point of reference for developers so they can see if their changes have broken anything. If you modify something in GPUVerify or add a new test you should re-generate the baseline.:: $ ./gvtester.py --write-pickle ./new-baseline.pickle testsuite $ ./gvtester.py -c testsuite/baseline.pickle ./new-baseline.pickle If the comparison looks good and you haven't broken anything then go ahead and replace the baseline pickle file.:: $ mv ./new-baseline.pickle testsuite/baseline.pickle Canonical path prefix --------------------- When pickle files are generated the full path to each kernel file is recorded. This could potentially make comparisions (``--compare-pickles``) difficult and different machines as the absolute paths are likely to be different. To work around this issue ``gvtester.py`` applies path Canonicalisation rules to the absolute path to each kernel file when using ``--compare-pickles``. These rules are: #. Remove all text leading up to the Canonical path prefix. #. Replace Windows slashes with UNIX ones. For example the two paths below refer to the same test. - ``/home/person/gpuverify/testsuite/OpenCL/typestest`` - ``c:\program files\gpuverify\testsuite\OpenCL\typestest`` The Canonicalisation rules reduce both of these paths to ``testsuite/OpenCL/typestest`` so they are considered the same test and are therefore compared. The default Canonical path prefix is ``testsuite`` but this can be changed at run time using ``--canonical-path-prefix``. Adding additional GPUVerify error codes --------------------------------------- ``gvtester.py`` directly imports the GPUVerify codes so that it is aware of the different error codes that it can return. An additional error condition (REGEX_MISMATCH_ERROR) can occur where everything passes but one or more regular expressions fail to match. ``gvtester.py`` has its own special error code for this. At run time ``gvtester.py`` will check there is no conflict between the GPUVerify error codes and REGEX_MISMATCH_ERROR. To add an error code simply add it to the ErrorCodes class in ``GPUVerify.py``. Make sure your new error code has a value larger than existing error codes. There is no need to regenerate the baseline unless you've changed the testsuite in some way.