Skip to content

Building from scratch

Jump to bottom
Mohamad Barbar edited this page Feb 21, 2022 · 6 revisions

These are instructions for building LLVM, SVF, and the assignments (Teaching-Software-Analysis) from scratch. This is useful if you like to work with your own editor or terminal or have trouble with Docker, the image, or VSCode (M1 Macs currently do).

0 - Pre-requisites

These instructions are for UNIX-y systems like Linux or macOS. Windows Subsystem for Linux might do as well.

1 - Install CMake

Install CMake through your package manager. Some possibilities (these commands may require use of sudo):

  • Debian and Ubuntu based systems
$ apt-get install cmake
  • macOS using Homebrew
$ brew install cmake
  • macOS using MacPorts
$ port install cmake

If you run into an error about permissions, prefix the command with sudo, e.g. sudo apt-get install cmake.

Alternatively, install CMake according to the CMake website (make sure to update your PATH to include cmake).

2 - Create a fresh directory

We will do everything in this directory.

$ mkdir software-verification
$ cd software-verification

3 - Build LLVM

Retrieve the LLVM sources and extract them.

$ curl -L https://github.com/llvm/llvm-project/releases/download/llvmorg-13.0.0/llvm-13.0.0.src.tar.xz > llvm.tar.xz
$ tar -xvf llvm.tar.xz

Create a directory to build LLVM in.

$ mkdir llvm-13-build
$ cd llvm-13-build

Configure.

$ cmake ../llvm-13.0.0.src/

Build. 8 can be replaced with the number of available CPU cores on your machine. On an 8GB M1 MacBook Air, this should take about 20 minutes.

$ make -j8

Save the full path to our LLVM build in a variable (which will be used to build SVF and Teaching-Software-Analysis later).

$ export LLVM_DIR=$(pwd)

Finally, move up a level.

$ cd ..

(Optional.) Delete the sources to save disk space. We've built what we need from them.

rm -r llvm.tar.xz

4 - Build Z3

Retrieve and extract the Z3 sources.

curl -L https://github.com/Z3Prover/z3/archive/refs/tags/z3-4.8.14.tar.gz > z3.tar.gz
tar -xvf z3.tar.gz

Create a directory to build Z3 in.

mkdir z3-build
cd z3-build

Configure.

cmake -DZ3_BUILD_LIBZ3_SHARED=false ../z3-z3-4.8.14

Build. Choose the argument to -j as before.

make -j8

Install.

mkdir install
make install DESTDIR=install

Export our Z3 directory like we did for LLVM.

export Z3_DIR="$(pwd)/install/usr/local"

Move up a level.

cd ..

(Optional.) Delete the archived sources to save disk space.

rm z3.tar.gz

5 - Build SVF

Grab the SVF sources.

$ git clone https://github.com/SVF-Tools/SVF.git
$ cd SVF

Build. This should take a few minutes.

$ ./build.sh

Save the full path to our SVF build in a variable (which will be used to build Teaching-Software-Analysis next).

$ export SVF_DIR=$(pwd)

Finally, move up a level.

$ cd ..

6 - Build Teaching-Software-Verification

Grab the Teaching-Software-Verification sources.

$ git clone https://github.com/SVF-tools/Teaching-Software-Verification
$ cd Teaching-Software-Verification

Configure. We use the Debug build type to make debugging your assignments easier.

$ cmake -DCMAKE_BUILD_TYPE=Debug .

Build.

$ make

Congratulations! All built.

7 - Running and debugging your assignments

If you take a peak in the bin directory, you can see your assignments, the hello world program, and the code graph program. To run the hello world program for example, you can

$ ./bin/hello

With your favourite text editor, you can modify the sources in directories like Assignment-1 or HelloWorld, run make again, and then rerun your programs.

To debug assignments, simply run your assignment with a debugger (like LLDB or GDB), for example:

$ lldb ./bin/hello

Some resources on LLDB:

8 - Build and debug in VSCode on Apple M1 (optional)

Install the CodeLLDB extension in VSCode. It looks like:

Still in the same Teaching-Software-Analysis directory we created in Section 5, replace the contents of:

  • .vscode/launch.json with:
{
    "version": "0.2.0",
    "configurations": [
        {
            "name": "(lldb) Launch",
            "type": "lldb",
            "request": "launch",
            // Please change to executable of your working assignment e.g. Assignment-1: assign-1
            "program": "${workspaceFolder}/bin/assign-3",
            "args": ["-stat=false"], // may input the test llvm bc file or other options may use
            "stopAtEntry": false,
            "cwd": "${workspaceFolder}",
            "environment": [],
            "MIMode": "lldb",
            "setupCommands": [
                {
                    "description": "Enable pretty-printing for gdb",
                    "text": "-enable-pretty-printing",
                    "ignoreFailures": true
                }
            ],
            "preLaunchTask": "C/C++: cpp build active file"
        }
    ]
}
  • .vscode/tasks.json with:
{
    "tasks": [
        {
            "label": "C/C++: cpp build active file",
            "type": "shell",
            "command": "make",
            "options": {
                "cwd": "${workspaceFolder}"
            },
            "group": {
                "kind": "build",
                "isDefault": true
            },
            "detail": "Task generated by Debugger."
        }
    ],
    "version": "2.0.0"
}
  • .vscode/c_cpp_properties.json with:
{
    "configurations": [
        {
            "name": "Linux",
            "includePath": [
                "${workspaceFolder}/../SVF/**",
                "${workspaceFolder}/**"
            ],
            "defines": [],
            "compilerPath": "/usr/bin/clang",
            "cStandard": "gnu11",
            "cppStandard": "gnu++14",
            "intelliSenseMode": "macos-clang-arm64",
            "macFrameworkPath": [
                "/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/System/Library/Frameworks"
            ]
        }
    ],
    "version": 4
}

Now you can follow Section 2 from the Docker/VSCode instructions.

Note: if an assertion is triggered, as is usually the case with failed test cases, the debugger will take you to some scary assembly (actually where the code stopped execution in some system library). Don't fret, you can still move around the call stack to someplace more familiar.

Clone this wiki locally