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 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
$ sudo apt-get update
$ sudo apt-get install -y cmake git gcc g++ libtinfo-dev libz-dev zip wget
- macOS using Homebrew. If you haven't installed Homebrew, run the following command in your terminal.
$ /bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"
If Homebrew is installed, run the following commands in your terminal.
$ brew install cmake git
This part is applicable to both Ubuntu/Debian and MacOS. Grab the SVF sources.
$ git clone https://github.com/SVF-Tools/SVF.git
$ cd SVF
Build. This should take a few minutes (LLVM build may take over 10 mins).
$ bash build.sh
Save the full path to our SVF build in a variable (which will be used to build Teaching-Software-Analysis next).
$ bash setup.sh
If success, you may see the output in the end like this:
SVF_DIR=/Users/z5489735/2023/Teaching/SVF
LLVM_DIR=/Users/z5489735/2023/Teaching/SVF/llvm-16.0.0.obj
Z3_DIR=/Users/z5489735/2023/Teaching/SVF/z3.obj
The SVF_DIR, LLVM_DIR, and Z3_DIR are the paths to the SVF source code, LLVM, and Z3 respectively. We will use these paths in the later step.
Finally, move up a level.
$ cd ..
This part is applicable to both Ubuntu/Debian and MacOS. 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.
This part is applicable to both Ubuntu/Debian and MacOS. Grab the SVF sources.
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:
VSCode is a source-code editor. This part is applicable to both Ubuntu/Debian and MacOS. Grab the SVF sources.
- Visual Studio Code is a source-code editor. It can be installed by downloading it from the official website
https://code.visualstudio.com/.
- Install the necessary extensions for C/C++ development in VSCode, like the Microsoft C/C++ extension for IntelliSense, debugging, and code browsing.
-
Setup VSCode CMake build
- Guide on how to set up the CMake build system within VSCode, including configuring tasks and launch JSON files for building and debugging.
- First, open the project under the project folder
Teaching-Software-Analysis. - Then, open the file
.vscode/tasks.jsonand add the following content.
The following is the default content.
{
"tasks": [
{
"label": "C/C++: cpp build active file",
"type": "shell",
"command": "cmake -DCMAKE_BUILD_TYPE=Debug -DSVF_DIR=/Users/z5489735/2023/Teaching/SVF -DLLVM_DIR=/Users/z5489735/2023/Teaching/SVF/llvm-16.0.0.obj -DZ3_DIR=/Users/z5489735/2023/Teaching/SVF/z3.obj . && make",
"options": {
"cwd": "${workspaceFolder}"
},
"group": {
"kind": "build",
"isDefault": true
},
"detail": "Task generated by Debugger."
}
],
"version": "2.0.0"
}We need to change the command field according to the installation path of LLVM and Z3. The SVF_DIR should be the path of the SVF source code. The LLVM_DIR and Z3_DIR should be the installation path of LLVM and Z3 respectively.
For example. If your LLVM_DIR is /Users/z5489735/2023/Teaching/SVF/llvm-16.0.0.obj and the Z3_DIR is /Users/z5489735/2023/Teaching/SVF/z3.obj, then the command field should be changed to cmake -DCMAKE_BUILD_TYPE=Debug -DSVF_DIR=/Users/z5489735/2023/SVF/ -DLLVM_DIR=/opt/homebrew/Cellar/llvm@16/16.0.6/ -DZ3_DIR=/Users/z5489735/2023/Teaching/SVF/z3.obj . && make.
And for launch.json, we need to change the gdb to lldb as the follwoing.
{
"version": "0.2.0",
"configurations": [
{
"name": "(lldb) Launch",
"type": "cppdbg",
"request": "launch",
"program": "${workspaceFolder}/bin/hello",
"args": [],
"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"
}
]
}Then Click Run And Debug and click the triangle button to start the build process.
If success you can see the following output from the DEBUG CONSOLE.
