Building Teaching Software Analysis Repo from scratch
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).
These instructions are for UNIX-y systems like Linux or macOS. Windows Subsystem for Linux might do as well.
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).
We will do everything in this directory.
$ mkdir software-verification
$ cd software-verification
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 directories to install and build LLVM in.
$ mkdir llvm-13
$ mkdir llvm-13-build
$ cd llvm-13-build
Configure.
$ cmake -DCMAKE_INSTALL_PREFIX="$(pwd)/../llvm-13" ../llvm-13.0.0.src/
Build and install. 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
$ make install
Move up a level.
$ cd ..
Save the full path to our LLVM build in a variable (which will be used to build SVF and Teaching-Software-Verification later).
$ export LLVM_DIR="$(pwd)/llvm-13"
(Optional.) Delete the sources and the build (we're keeping the install) to save disk space. We've built what we need from them.
rm -r llvm.tar.xz llvm-13.0.0.src llvm-13-build
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 directories to install and build Z3 in.
$ mkdir z3
$ mkdir z3-build
$ cd z3-build
Configure.
$ cmake -DCMAKE_INSTALL_PREFIX="$(pwd)/../z3" -DZ3_BUILD_LIBZ3_SHARED=false ../z3-z3-4.8.14
Build and install. Choose the argument to -j as before.
$ make -j8
$ make install
Move up a level.
$ cd ..
Export our Z3 directory like we did for LLVM.
$ export Z3_DIR="$(pwd)/z3"
(Optional.) Delete the sources and build to save disk space.
$ rm -r z3.tar.gz z3-build z3-z3-4.8.14
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-Verification next).
$ export SVF_DIR=$(pwd)
Finally, move up a level.
$ cd ..
Grab the Teaching-Software-Analysis sources.
$ git clone https://github.com/SVF-tools/Teaching-Software-Analysis
$ cd Teaching-Software-Analysis
Configure. We use the Debug build type to make debugging your assignments easier.
$ cmake -DCMAKE_BUILD_TYPE=Debug .
Build.
$ make
Congratulations! All built.
If you take a peak in the bin directory, you can see your assignments, the hello world program, and the svfir 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 from the Teaching-Software-Verification directory, 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:
Install the CodeLLDB extension in VSCode. It looks like:
Still in the same Teaching-Software-Verification directory we created in Section 5, replace the contents of:
-
.vscode/launch.jsonwith:
{
"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.jsonwith:
{
"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.jsonwith:
{
"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
}
-
.vscode/settings.jsonwith:
(i.e., make it empty.)
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.
