SVF

https://github.com/svf-tools/svf
Admin
SVF is a static value-flow analysis tool for LLVM-based languages.
Tokens:42,648
Snippets:479
Trust Score:6.5
Update:4 months ago
Show doc for...
Tokens:
Raw
### Install gllvm

Source: https://github.com/svf-tools/svf/wiki/Compile-bitcode-file-using-wllvm-gclang

Steps to install gllvm, including Go tool installation and dependency retrieval. Ensure the PATH is updated to include the go bin directory.

```bash
wget https://go.dev/dl/go1.16.15.linux-amd64.tar.gz
```

```bash
rm -rf /usr/local/go && tar -C /usr/local -xzf go1.16.15.linux-amd64.tar.gz
```

```bash
export PATH=$PATH:/usr/local/go/bin
```

```bash
go version
```

```bash
GO111MODULE=off go get github.com/SRI-CSL/gllvm/cmd/...
```

--------------------------------

### Install Library Requirements

Source: https://github.com/svf-tools/svf/wiki/Install-LLVM-Gold-Plugin-on-Ubuntu

Installs necessary development headers and tools for building LLVM and binutils.

```bash
sudo apt-get install linux-headers-$(uname -r) git g++ gcc cmake bash csh gawk automake libtool bison flex libncurses5-dev
```

--------------------------------

### Configure and Install SVF Tools

Source: https://github.com/svf-tools/svf/blob/master/svf-llvm/tools/CMakeLists.txt

Iterates through the list of all SVF tools to configure build properties and installation rules. This includes linking libraries, setting output directories, and defining installation destinations.

```cmake
foreach(_tool IN LISTS ALL_TOOLS)
  # Link the SvfLLVM library against SVF's core & LLVM libraries
  target_link_libraries(${_tool} PRIVATE SvfCore SvfLLVM)

  # Ensure that the build artifacts are placed into lib/bin/include relative to the top of the build directory
  set_target_properties(
    ${_tool}
    PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${SVF_BINARY_DIR}/bin
               LIBRARY_OUTPUT_DIRECTORY ${SVF_BINARY_DIR}/lib
               ARCHIVE_OUTPUT_DIRECTORY ${SVF_BINARY_DIR}/lib
  )

  install(
    TARGETS ${_tool}
    EXPORT SVFTargets
    RUNTIME DESTINATION ${SVF_INSTALL_BINDIR}
    LIBRARY DESTINATION ${SVF_INSTALL_LIBDIR}
    ARCHIVE DESTINATION ${SVF_INSTALL_LIBDIR}
            FILE_SET HEADERS
            DESTINATION ${SVF_INSTALL_INCLUDEDIR}
  )
endforeach()
```

--------------------------------

### Install Missing makeinfo

Source: https://github.com/svf-tools/svf/wiki/Install-LLVM-Gold-Plugin-on-Ubuntu

Installs 'makeinfo' if it's not found, which is required for some build processes.

```bash
sudo apt-get install apt-file texinfo texi2html
sudo apt-file update
sudo apt-file search makeinfo
```

--------------------------------

### Setup SVF in Docker

Source: https://github.com/svf-tools/svf/wiki/Try-SVF-in-Docker

Execute the setup script to configure SVF within the running Docker container.

```bash
. ./setup.sh
```

--------------------------------

### Install SVF Core Library Files

Source: https://github.com/svf-tools/svf/blob/master/svf/CMakeLists.txt

Installs the built SvfCore library targets and headers to the specified installation directories.

```cmake
install(
  TARGETS SvfCore
  EXPORT SVFTargets
  RUNTIME DESTINATION ${SVF_INSTALL_BINDIR}
  LIBRARY DESTINATION ${SVF_INSTALL_LIBDIR}
  ARCHIVE DESTINATION ${SVF_INSTALL_LIBDIR}
          FILE_SET HEADERS
          DESTINATION ${SVF_INSTALL_INCLUDEDIR}
)
```

--------------------------------

### Install wllvm

Source: https://github.com/svf-tools/svf/wiki/Compile-bitcode-file-using-wllvm-gclang

Install wllvm using pip. This provides commands like wllvm, wllvm++, extract-bc, and wllvm-sanity-checker.

```bash
pip install wllvm
```

--------------------------------

### Install ExtAPI Bitcode File

Source: https://github.com/svf-tools/svf/blob/master/svf-llvm/CMakeLists.txt

Installs the generated extapi.bc file to the specified destination directory with a specific rename.

```cmake
install(
  FILES ${SVF_BUILD_EXTAPI_BC}
  DESTINATION ${SVF_INSTALL_EXTAPIDIR}
  RENAME ${SVF_EXTAPI_BC_NAME}
)
```

--------------------------------

### Install SVF using npm

Source: https://github.com/svf-tools/svf/wiki/Setup-Guide

Install the SVF library via npm. This is a quick way to get SVF if you are working within an npm-based project.

```bash
npm i svf-lib
```

--------------------------------

### Set Up SVF Environment (Release)

Source: https://github.com/svf-tools/svf/wiki/User-Guide

Sets up the SVF environment variables to point to the release version executables. Navigate to the SVF home directory and source the setup script.

```bash
cd $SVF_HOME
. ./setup.sh
```

--------------------------------

### Generate and Install Config Header

Source: https://github.com/svf-tools/svf/blob/master/CMakeLists.txt

Generates the config.h file into the build tree and installs it to the specified include directory.

```cmake
configure_file(${SVF_SOURCE_DIR}/cmake/SVFConfigHdr.cmake.in ${SVF_BINARY_DIR}/include/Util/config.h @ONLY)
install(FILES ${SVF_BINARY_DIR}/include/Util/config.h DESTINATION ${SVF_INSTALL_INCLUDEDIR}/Util)
```

--------------------------------

### Generate and Install Pkgconf Package Configuration

Source: https://github.com/svf-tools/svf/blob/master/CMakeLists.txt

Generates the SVF.pc file for pkgconf in the build tree and installs it to the specified pkgconfig directory.

```cmake
configure_file(cmake/SVF.pc.in ${SVF_BINARY_DIR}/lib/pkgconfig/SVF.pc @ONLY)
install(FILES ${SVF_BINARY_DIR}/lib/pkgconfig/SVF.pc DESTINATION ${SVF_INSTALL_PKGCONFDIR})
```

--------------------------------

### Install LLVM Gold Plugin and LTO Libraries

Source: https://github.com/svf-tools/svf/wiki/Install-LLVM-Gold-Plugin-on-Ubuntu

Copies the compiled LLVMGold.so plugin and LTO libraries to the bfd-plugins directory.

```bash
cd /usr/lib
sudo mkdir bfd-plugins
cd bfd-plugins
sudo cp ~/llvm-6.0.0.obj/lib/LLVMgold.so ./
sudo cp ~/llvm-6.0.0.obj/lib/libLTO.* ./
```

--------------------------------

### Install Firefox Build Prerequisites

Source: https://github.com/svf-tools/svf/wiki/Compiling-Firefox

Installs necessary packages for building Firefox, including Rust, Cargo, autoconf2.13, and various development libraries.

```bash
$ sudo apt-get install rustc cargo autoconf2.13 libgtk-3-dev libgconf2-dev libdbus-glib-1-dev libpulse-dev yasm
```

--------------------------------

### Configure and build a C project with WLLVM

Source: https://github.com/svf-tools/svf/wiki/Detecting-memory-leaks

Prepare a C project for compilation into LLVM bitcode by configuring and building it with WLLVM. Ensure necessary development libraries are installed.

```bash
sudo apt install libglib2.0-dev libncurses5 libtool
wget https://pkgconfig.freedesktop.org/releases/pkg-config-0.26.tar.gz
tar xf pkg-config-0.26.tar.gz
cd pkg-config-0.26

export LLVM_COMPILER=clang
CC=wllvm ./configure
make
```

--------------------------------

### Compile RIOT Example with gclang

Source: https://github.com/svf-tools/svf/wiki/Compile-bitcode-file-using-wllvm-gclang

Compile the RIOT OS default example using gclang and gclang++. The -save-temps=obj flag is used to preserve intermediate files, including bitcode.

```bash
git clone https://github.com/RIOT-OS/RIOT
cd RIOT/examples/default/
make CC="gclang -O0 -Xclang -disable-O0-optnone -g -save-temps=obj -fno-discard-value-names -w" CXX="gclang++ -O0 -Xclang -disable-O0-optnone -g -save-temps=obj -fno-discard-value-names -w" -j8
```

--------------------------------

### Install SvfLLVM Library Files

Source: https://github.com/svf-tools/svf/blob/master/svf-llvm/CMakeLists.txt

Installs the SvfLLVM library files to the configured installation tree, including runtime binaries, libraries, and headers. This makes the library available for external use after building.

```cmake
install(
  TARGETS SvfLLVM
  EXPORT SVFTargets
  RUNTIME DESTINATION ${SVF_INSTALL_BINDIR}
  LIBRARY DESTINATION ${SVF_INSTALL_LIBDIR}
  ARCHIVE DESTINATION ${SVF_INSTALL_LIBDIR}
          FILE_SET HEADERS
          DESTINATION ${SVF_INSTALL_INCLUDEDIR}
)
```

--------------------------------

### Example Command and Output

Source: https://github.com/svf-tools/svf/wiki/Quick-benchmarking-script

Demonstrates how to execute the benchmarking script with specific SVF binary, argument sets, resource limits, and bitcode files. The output shows a detailed comparison table of time and memory usage between the two argument sets for each bitcode file, along with their geometric means.

```shell
$ ./bench.sh ~/clone/svf-upstream/Release-build/bin/wpa "-fspta -marked-clocks-only" "-vfspta -marked-clocks-only -node-alloc-strat=dense -ptd=persistent" 5 20 ~/bitcode/gnuplot.bc ~/bitcode/tmux.bc ~/bitcode/i3.bc
```

```text
  = args = 
    svf binary    : /home/mbarbar/clone/svf-upstream/Release-build/bin/wpa
    args1         : -fspta -marked-clocks-only
    args2         : -vfspta -marked-clocks-only -node-alloc-strat=dense -ptd=persistent
    time limit    : 5 hours
    memory limit  : 20 gigabytes
    bitcode files : /home/mbarbar/bitcode/gnuplot.bc /home/mbarbar/bitcode/tmux.bc /home/mbarbar/bitcode/i3.bc (3)
┌──────────────────────────────────┬───────────────────────┬───────────────────────┬───────────────────────────┐
│                                  │         ARGS 1        │         ARGS 2        │      Difference (1/2)     │
│                          Program ├┄┄┄┄┄┄┄┄┄┄┄┄┬┄┄┄┄┄┄┄┄┄┄┼┄┄┄┄┄┄┄┄┄┄┄┄┬┄┄┄┄┄┄┄┄┄┄┼┄┄┄┄┄┄┄┄┄┄┄┄┄┬┄┄┄┄┄┄┄┄┄┄┄┄┄┤
│                                  │       Time │   Memory │       Time │   Memory │        Time │      Memory │
├──────────────────────────────────┼────────[s]─┼─────[GB]─┼────────[s]─┼─────[GB]─┼─────────────┼─────────────┤
│ /home/mbarbar/bitcode/gnuplot.bc │     131.12 │     3.92 │      89.34 │     2.73 │       1.47x │       1.43x │
│    /home/mbarbar/bitcode/tmux.bc │     257.81 │     8.08 │      82.92 │     3.05 │       3.11x │       2.65x │
│      /home/mbarbar/bitcode/i3.bc │       5.33 │     0.47 │       4.74 │     0.42 │       1.12x │       1.11x │
├──────────────────────────────────┼───────────────────────────────────────────────┼─────────────┼─────────────┤
│                        Geo. Mean │                                               │       2.26x │       2.05x │
└──────────────────────────────────┴───────────────────────────────────────────────┴─────────────┴─────────────┘
```

--------------------------------

### Install Build Dependencies

Source: https://github.com/svf-tools/svf/wiki/Compiling-Chrome-using-flto

Install the required build dependencies for Chromium on your system. This script handles package installations.

```bash
$ build/install-build-deps.sh
```

--------------------------------

### Install Generated CMake Configuration Files

Source: https://github.com/svf-tools/svf/blob/master/CMakeLists.txt

Installs the generated `SVFConfig.cmake` and `SVFConfigVersion.cmake` files to the package configuration directory.

```cmake
install(FILES ${SVF_BINARY_DIR}/lib/cmake/SVF/SVFConfig.cmake DESTINATION ${SVF_INSTALL_CMAKECONFIGDIR})
```

```cmake
install(FILES ${SVF_BINARY_DIR}/lib/cmake/SVF/SVFConfigVersion.cmake DESTINATION ${SVF_INSTALL_CMAKECONFIGDIR})
```

--------------------------------

### Install SVF Targets Configuration

Source: https://github.com/svf-tools/svf/blob/master/CMakeLists.txt

Installs the exported SVF targets configuration file to the designated installation directory, making them available for external projects.

```cmake
install(
  EXPORT SVFTargets
  NAMESPACE SVF::
  DESTINATION ${SVF_INSTALL_CMAKECONFIGDIR}
)
```

--------------------------------

### Memory SSA Output Example

Source: https://github.com/svf-tools/svf/wiki/Analyze-a-Simple-C-Program

An example of the Memory SSA output for the 'swap' function and 'main' function, detailing memory operations and points-to sets.

```text
==========FUNCTION: swap==========
2V_1 = ENCHI(MR_2V_0) 	pts{22 }
4V_1 = ENCHI(MR_4V_0) 	pts{24 }
entry

LDMU(MR_2V_1) 	pts{22 }
  %0 = load i8** %p, align 8

LDMU(MR_4V_1) 	pts{24 }
  %1 = load i8** %q, align 8
  store i8* %1, i8** %p, align 8
2V_2 = STCHI(MR_2V_1) 	pts{22 }

  store i8* %0, i8** %q, align 8
4V_2 = STCHI(MR_4V_1) 	pts{24 }

  ret void
RETMU(MR_2V_2) 	pts{22 }
RETMU(MR_4V_2) 	pts{24 }

==========FUNCTION: main==========
2V_1 = ENCHI(MR_2V_0) 	pts{22 }
4V_1 = ENCHI(MR_4V_0) 	pts{24 }
entry
  %a1 = alloca i8, align 1
  %b1 = alloca i8, align 1
  %a = alloca i8*, align 8
  %b = alloca i8*, align 8
  store i8* %a1, i8** %a, align 8
2V_2 = STCHI(MR_2V_1) 	pts{22 }

  store i8* %b1, i8** %b, align 8
4V_2 = STCHI(MR_4V_1) 	pts{24 }

CALMU(MR_2V_2) 	pts{22 }
CALMU(MR_4V_2) 	pts{24 }
  call void @swap(i8** %a, i8** %b) CallSite:   call void @swap(i8** %a, i8** %b)
2V_3 = CALCHI(MR_2V_2) 	pts{22 }
4V_3 = CALCHI(MR_4V_2) 	pts{24 }

  ret i32 0
RETMU(MR_2V_3) 	pts{22 }
RETMU(MR_4V_3) 	pts{24 }

```

--------------------------------

### Install SVF Dependencies

Source: https://github.com/svf-tools/svf/wiki/Set-up-the-Debugging-Environment-for-SVF-in-VSCode

Installs necessary libraries for building SVF on an Ubuntu system. Ensure you have CMake, GCC, G++, and other development tools.

```bash
sudo apt install cmake gcc g++ libtinfo-dev libz-dev zip wget
```

--------------------------------

### Example: ALLOC_ARG Annotation for Parameter Allocation

Source: https://github.com/svf-tools/svf/wiki/Handling-External-APIs-with-extapi.c

Illustrates the use of the ALLOC_ARGi annotation to indicate that a function allocates memory and stores it in its i-th parameter.

```c
__attribute__((annotate("ALLOC_ARG0")))
int db_create(void **dbp, void *dbenv, unsigned int flags)
{
    return 0;
}
```

--------------------------------

### Example C Code for Analysis

Source: https://github.com/svf-tools/svf/wiki/Specifications-in-ExtAPI.json

This C code defines a function 'foo' and its usage in 'main'. It serves as an example for demonstrating how ExtAPI.json can be used to override function definitions during SVF analysis.

```c
char* foo(char* arg)
{
    return arg;
}

int main()
{
    char* ret = foo("abc");
    return 0;
}
```

--------------------------------

### Set Build Arguments for Chromium

Source: https://github.com/svf-tools/svf/wiki/Compiling-Chrome-using-flto

Configure build arguments by editing the 'args.gn' file. This example sets up a release build with component build enabled and specifies the path to the local Clang.

```gn
is_debug = false
is_component_build = true
symbol_level = 0
enable_nacl = false
clang_base_path = "PATH_TO_LLVM_BUILD"
clang_use_chrome_plugins = false
clang_version = "7.0.0"
```

--------------------------------

### Compile teeworlds Example with wllvm

Source: https://github.com/svf-tools/svf/wiki/Compile-bitcode-file-using-wllvm-gclang

Compile teeworlds version 0.7.5 using wllvm and wllvm++. CMake is used for configuration and building. Bitcode is extracted from the teeworlds executable.

```bash
wget https://github.com/teeworlds/teeworlds/releases/download/0.7.5/teeworlds-0.7.5-src.tar.gz
tar -xzvf teeworlds-0.7.5-src.tar.gz
mkdir teeworlds-0.7.5-src/build && cd teeworlds-0.7.5-src/build
CC="wllvm -O0 -Xclang -disable-O0-optnone -g -save-temps=obj -fno-discard-value-names -w" CXX="wllvm++ -O0 -Xclang -disable-O0-optnone -g -save-temps=obj -fno-discard-value-names -w" cmake ../
make -j12
```

```bash
extract-bc teeworlds
```

--------------------------------

### Check gllvm Environment

Source: https://github.com/svf-tools/svf/wiki/Compile-bitcode-file-using-wllvm-gclang

Set the LLVM path to LLVM14 and run gsanity-check to verify the environment setup for gllvm.

```bash
export LLVM_COMPILER_PATH=$SVF_INSTALL_LLVM_14/bin
gsanity-check
```

--------------------------------

### Compile redis Example with wllvm

Source: https://github.com/svf-tools/svf/wiki/Compile-bitcode-file-using-wllvm-gclang

Compile redis version 7.0.11 using wllvm and wllvm++. Standard make is used for building. Bitcode is extracted from the redis-server and redis-cli binaries.

```bash
wget https://github.com/redis/redis/archive/refs/tags/7.0.11.tar.gz
tar -xzvf 7.0.11.tar.gz
cd redis-7.0.11/
CC="wllvm -O0 -Xclang -disable-O0-optnone -g -save-temps=obj -fno-discard-value-names -w" CXX="wllvm++ -O0 -Xclang -disable-O0-optnone -g -save-temps=obj -fno-discard-value-names -w" make -j12
```

```bash
cd src && extract-bc redis-server
cd src && extract-bc redis-cli
```

--------------------------------

### Compile darknet Example with wllvm

Source: https://github.com/svf-tools/svf/wiki/Compile-bitcode-file-using-wllvm-gclang

Compile darknet using wllvm and wllvm++. The Makefile needs to be edited to set CC=wllvm and CPP=wllvm++. Bitcode is extracted from the darknet executable.

```bash
git clone https://github.com/pjreddie/darknet.git
cd darknet/
vim Makefile
CC="wllvm -O0 -Xclang -disable-O0-optnone -g -save-temps=obj -fno-discard-value-names -w" CXX="wllvm++ -O0 -Xclang -disable-O0-optnone -g -save-temps=obj -fno-discard-value-names -w" make -j12
```

```bash
extract-bc darknet
```

--------------------------------

### Compile NanoMQ Example with wllvm

Source: https://github.com/svf-tools/svf/wiki/Compile-bitcode-file-using-wllvm-gclang

Compile NanoMQ version 0.17.2 using wllvm and wllvm++. This involves cloning a submodule, configuring with CMake, and then extracting bitcode for the main binaries.

```bash
wget https://github.com/emqx/nanomq/archive/refs/tags/0.17.2.tar.gz
tar -xzvf 0.17.2.tar.gz
cd nanomq-0.17.2/nng/
git clone https://github.com/nanomq/NanoNNG.git
cd NanoNNG/ && git checkout 0.17.2
cmake ./ && make -j12
mv * ../
cd ../../build
CC="wllvm -O0 -Xclang -disable-O0-optnone -g -save-temps=obj -fno-discard-value-names -w" CXX="wllvm++ -O0 -Xclang -disable-O0-optnone -g -save-temps=obj -fno-discard-value-names -w" cmake ../
make -j12
```

```bash
extract-bc nanomq/nanomq
extract-bc nanomq_cli/nanomq_cli
```

--------------------------------

### Start Stopped Docker Container

Source: https://github.com/svf-tools/svf/wiki/Try-SVF-in-Docker

Start a Docker container that has been previously stopped. Replace 'your_container_name' with the actual container name or ID.

```bash
docker start "your_container_name"
```

--------------------------------

### Example: MEMSET Annotation for Memory Set Operations

Source: https://github.com/svf-tools/svf/wiki/Handling-External-APIs-with-extapi.c

Demonstrates the MEMSET annotation for functions that perform memory set operations, akin to memset.

```c
__attribute__((annotate("MEMSET")))
void llvm_memset_p0i8_i64(char* dst, char elem, int sz, int flag)
{
}
```

--------------------------------

### Compile mp4v2 Example with wllvm

Source: https://github.com/svf-tools/svf/wiki/Compile-bitcode-file-using-wllvm-gclang

Compile version 2.1.3 of mp4v2 using wllvm and wllvm++. CMake is used as the build system. Ensure to run extract-bc for each target binary.

```bash
wget https://github.com/enzo1982/mp4v2/archive/refs/tags/v2.1.3.tar.gz
tar -xzvf v2.1.3.tar.gz
cd mp4v2-2.1.3
mkdir build && cd build
CC="wllvm -O0 -Xclang -disable-O0-optnone -g -save-temps=obj -fno-discard-value-names -w" CXX="wllvm++ -O0 -Xclang -disable-O0-optnone -g -save-temps=obj -fno-discard-value-names -w" cmake ../
make -j12
```

```bash
extract-bc mp4art && extract-bc mp4extract && extract-bc mp4file && extract-bc mp4subtitle && extract-bc mp4track
```

--------------------------------

### AppDef Function Definition Example

Source: https://github.com/svf-tools/svf/wiki/Handling-External-APIs-with-extapi.c

A C code snippet defining a function 'foo' in the application module. This serves as an example for demonstrating how SVF handles function definitions and their potential overwriting by external definitions.

```c
AppDef: char* foo(char *a, char *b)
        {
           return a;
        }
```

--------------------------------

### Set LLVM and Clang Environment Paths

Source: https://github.com/svf-tools/svf/wiki/Setup-Guide-(CMake)

Configures the environment variables to point to the LLVM and Clang installation directory and adds their binaries to the system's PATH. Replace 'your_path_to_clang+llvm-10.0.0-x86_64-linux-gnu-ubuntu-18.04' with the actual path.

```bash
export LLVM_DIR=your_path_to_clang+llvm-10.0.0-x86_64-linux-gnu-ubuntu-18.04
export PATH=$LLVM_DIR/bin:$PATH
```

--------------------------------

### Run SVF Docker Container

Source: https://github.com/svf-tools/svf/wiki/Try-SVF-in-Docker

Import the SVF Docker image and start an interactive bash session within the container.

```bash
docker run -i -t svftools/svf /bin/bash
```

--------------------------------

### GepStmt Example

Source: https://github.com/svf-tools/svf/wiki/Specifications-in-ExtAPI.json

Defines a function using two GepStmt operations. It first performs a GEP on the first argument (Arg0) to a dummy node, then performs another GEP on the dummy node to the return value.

```json
"_ZNSt5arrayIPK1ALm2EE4backEv":{
        "return":  "%class.A** ",
        "arguments":  "(%struct.std::array *)",
        "type": "CPP_EFT_DYNAMIC_CAST",
        "overwrite_app_function": 1,
        "GepStmt1": {
            "src": "Arg0",
            "dst": "Dummy",
            "offset": "0"
        },
        "GepStmt2": {
            "src": "Dummy",
            "dst": "Ret",
            "offset": "0"
        }
      }
```

--------------------------------

### Example: ALLOC_RET Annotation for Return Value Allocation

Source: https://github.com/svf-tools/svf/wiki/Handling-External-APIs-with-extapi.c

Demonstrates using the ALLOC_RET annotation to signify that a function allocates memory for its return value, which SVF then processes.

```c
__attribute__((annotate("ALLOC_RET")))
void *malloc(unsigned long size)
{
    return NULL;
}
```

--------------------------------

### CallStmt and ReturnStmt Example

Source: https://github.com/svf-tools/svf/wiki/Specifications-in-ExtAPI.json

Defines a function 'swapExtCallStmt' that involves a 'swap' function call. It copies arguments, loads values, and manages return values through a series of CopyStmt and LoadStmt operations.

```json
"swapExtCallStmt":{
        "return":  "void",
        "arguments":  "(char **, char **)",
        "type": "EFT_NOOP",
        "overwrite_app_function": 0,
        "CallStmt": {
            "callee_name": "swap",
            "callee_return": "void",
            "callee_arguments": "(char **, char **)",
            "CopyStmt1": {
                "src": "swapExtCallStmt_Arg0",
                "dst": "x"
            },
            "LoadStmt1": {
                "src": "x",
                "dst": "swap_Arg0"
            },
            "CopyStmt2": {
                "src": "swapExtCallStmt_Arg1",
                "dst": "swap_Arg1"
            },
             "ReturnStmt": {
                "src": "swap_Ret",
                "dst": "swapExtCallStmt_Ret"
            }
        }
      }
```

--------------------------------

### Compile C to LLVM IR and run mem2Reg

Source: https://github.com/svf-tools/svf/wiki/Analyze-a-Simple-C-Program

These commands compile a C file to LLVM IR and then apply the mem2Reg optimization pass. Ensure wllvm is installed for bc generation.

```bash
clang -S -c -Xclang -disable-O0-optnone -fno-discard-value-names -emit-llvm swap.c -o swap.ll
opt -S -p=mem2reg swap.ll -o swap.ll
```

--------------------------------

### Git Rebase to a Certain Commit

Source: https://github.com/svf-tools/svf/wiki/Git-command-lines

Interactively rebase commits starting from a specific commit ID. This example shows how to squash two commits into one.

```bash
git rebase -i commitId
```

```text
pick e06b526 dyn lib 18.04 ubuntu
pick 154a03f6 update bc files
pick ac9c1fd4 Update build.sh
```

```text
pick e06b526 dyn lib 18.04 ubuntu
s 154a03f6 update bc files
s ac9c1fd4 Update build.sh
```

```bash
git push -f
```

--------------------------------

### Example: Function Body Implementation for Side-Effects

Source: https://github.com/svf-tools/svf/wiki/Handling-External-APIs-with-extapi.c

This snippet shows how a function body in extapi.c can capture side-effects, like returning a pointer to a buffer, eliminating the need for the full function implementation.

```c
char *asctime_r(const void *tm, char *buf)
{
    return buf;
}
```

--------------------------------

### Set Up Git Repository

Source: https://github.com/svf-tools/svf/wiki/Git-command-lines

Clone a repository and configure global user information for commits.

```bash
git clone https://github.com/SVF-tools/SVF.git
git config --global user.name "Your name"
git config --global user.email "youremail@gmail.com"
```

--------------------------------

### Collect Uses on VFG

Source: https://github.com/svf-tools/svf/wiki/A-simple-driver-example-of-SVF

An example function to collect all uses of a definition of a value along the Value-Flow Graph (VFG). It traverses the VFG starting from a given value's definition.

```cpp
/*!
 * An example to query/collect all the uses of a definition of a value along value-flow graph (VFG)
 */
void collectUsesOnVFG(const SVFG* vfg, Value* val){
	PAG* pag = PAG::getPAG();

    PAGNode* pNode = pag->getPAGNode(pag->getValueNode(val));
    const VFGNode* vNode = vfg->getDefSVFGNode(pNode);
    FIFOWorkList<const VFGNode*> worklist;
    std::set<const VFGNode*> visited;
    worklist.push(vNode);

    /// Traverse along VFG
    while(!worklist.empty()){
    	const VFGNode* vNode = worklist.pop();
    	for(VFGNode::const_iterator it = vNode->OutEdgeBegin(), eit = vNode->OutEdgeEnd(); it!=eit; ++it) {
            if(visited.find(vNode)==visited.end()){
            	visited.insert(vNode);
            	worklist.push(vNode);
            }
    	}
    }

    /// Collect all LLVM Values
    for(std::set<const VFGNode*>::const_iterator it = visited.begin(), eit = visited.end(); it!=eit; ++it){
    	const VFGNode* node = *it;
    	/// can only query VFGNode involving top-level pointers (starting with % or @ in LLVM IR)
    	/// PAGNode* pNode = vfg->getLHSTopLevPtr(node);
    	/// Value* val = pNode->getValue();
    }
}


```

--------------------------------

### Example: OVERWRITE Annotation for Function Overwriting

Source: https://github.com/svf-tools/svf/wiki/Handling-External-APIs-with-extapi.c

Illustrates the OVERWRITE annotation, which allows a new function definition in extapi.c to replace an existing function definition within the application.

```c
__attribute__((annotate("OVERWRITE")))
void foo(char* arg)
{
    ...
    ...
}
```

--------------------------------

### Run Build Hooks

Source: https://github.com/svf-tools/svf/wiki/Compiling-Chrome-using-flto

Execute gclient runhooks to set up the build environment and download any remaining necessary components.

```bash
$ gclient runhooks
```

--------------------------------

### LoadStmt and StoreStmt Example

Source: https://github.com/svf-tools/svf/wiki/Specifications-in-ExtAPI.json

Defines a function with LoadStmt and StoreStmt side-effects. It loads the second argument (Arg1) into a dummy node and then stores the dummy node's value into the first argument (Arg0).

```json
"_ZNSsC1ERKSs":{
           "return":  "void",
           "arguments":  "(std::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)",
           "type": "CPP_EFT_A0R_A1R",
           "overwrite_app_function": 0,
           "LoadStmt": {
               "src": "Arg1",
               "dst": "Dummy"
           },
           "StoreStmt": {
               "src": "Dummy",
               "dst": "Arg0"
           }
       }
```

--------------------------------

### Configure and Build SVF (Release)

Source: https://github.com/svf-tools/svf/wiki/Setup-Guide-(Autoconf)

Run the configure script and then make in the SVF source root to build the release version of SVF.

```bash
./configure && make
```

--------------------------------

### Configure and Build LLVM

Source: https://github.com/svf-tools/svf/wiki/Setup-Guide-(Autoconf)

Create a build directory for LLVM, navigate into it, and run the configure script. The make command builds LLVM; use ENABLE_OPTIMIZED=0 for a debug build.

```bash
mkdir llvm-3.8.0.obj
cd llvm-3.8.0.obj
../llvm-3.8.0.src/configure --enable-assertions
make -j8  (or make -j8 ENABLE_OPTIMIZED=0 for debug version)
```

--------------------------------

### Install SvfFlags Target

Source: https://github.com/svf-tools/svf/blob/master/CMakeLists.txt

Installs the SvfFlags target and exports it under the name SVFTargets for use by other CMake projects.

```cmake
install(TARGETS SvfFlags EXPORT SVFTargets)
```

--------------------------------

### Configure and Build SVF (Debug)

Source: https://github.com/svf-tools/svf/wiki/Setup-Guide-(Autoconf)

Run the configure script and then make with ENABLE_OPTIMIZED=0 to build the debug version of SVF. A debug version of LLVM is not required.

```bash
./configure && make ENABLE_OPTIMIZED=0
```

--------------------------------

### Configure Binutils Build

Source: https://github.com/svf-tools/svf/wiki/Install-LLVM-Gold-Plugin-on-Ubuntu

Configures the binutils build with options to enable the Gold linker and plugins, disabling warnings.

```bash
mkdir build
cd build
../binutils/configure --enable-gold --enable-plugins --disable-werror
make
```

--------------------------------

### Introducing svf__main for Command Line Input

Source: https://github.com/svf-tools/svf/wiki/Handling-External-APIs-with-extapi.c

Demonstrates the use of svf__main in extapi.c to support main functions that require command-line arguments (argc, argv). These arguments are passed as abstract symbols for subsequent processing.

```c
ExtDecl: declare main();

ExtDef: void svf__main()
          {
              main();
          }

AppDef: int main() {

         }
```

--------------------------------

### Install CMake Module Finding Package Definitions

Source: https://github.com/svf-tools/svf/blob/master/CMakeLists.txt

Installs CMake module files, such as `FindZ3.cmake`, into the package configuration directory. This allows for finding external dependencies.

```cmake
configure_file(cmake/Modules/FindZ3.cmake ${SVF_BINARY_DIR}/lib/cmake/SVF/FindZ3.cmake @ONLY)
```

```cmake
install(
  DIRECTORY "${CMAKE_CURRENT_LIST_DIR}/cmake/Modules"
  DESTINATION "${SVF_INSTALL_CMAKECONFIGDIR}"
  FILES_MATCHING
  PATTERN "*.cmake"
)
```

--------------------------------

### Download Binutils Source

Source: https://github.com/svf-tools/svf/wiki/Install-LLVM-Gold-Plugin-on-Ubuntu

Clones the binutils-gdb repository to obtain the source code for building.

```bash
cd ~
git clone --depth 1 git://sourceware.org/git/binutils-gdb.git binutils
```

--------------------------------

### Build Firefox

Source: https://github.com/svf-tools/svf/wiki/Compiling-Firefox

Initiates the Firefox build process using the mach build command.

```bash
$ ./mach build
```

--------------------------------

### Link Directories for SvfFlags Target

Source: https://github.com/svf-tools/svf/blob/master/CMakeLists.txt

Specifies interface-specific link directories for the SvfFlags target, differentiating between build and install trees.

```cmake
target_link_directories(
  SvfFlags
  INTERFACE $<BUILD_INTERFACE:${SVF_BINARY_DIR}>
  INTERFACE $<BUILD_INTERFACE:${SVF_BINARY_DIR}/lib>
  INTERFACE $<INSTALL_INTERFACE:${SVF_INSTALL_LIBDIR}>
)
```

--------------------------------

### Example: MEMCPY Annotation for Memory Copy Operations

Source: https://github.com/svf-tools/svf/wiki/Handling-External-APIs-with-extapi.c

This snippet uses the MEMCPY annotation to denote functions with side-effects similar to memcpy.

```c
__attribute__((annotate("MEMCPY")))
void *memmove(void *str1, const void *str2, unsigned long n)
{
    return NULL;
}
```

--------------------------------

### Build CPU2017 Benchmarks with WLLVM

Source: https://github.com/svf-tools/svf/wiki/Compiling-CPU2000-2006-2017

This command cleans previous builds and then builds specified CPU2017 benchmarks using WLLVM. Ensure you are in the $CPU2017_HOME directory and have sourced the shrc file.

```bash
cd $CPU2017_HOME
. ./shrc
runcpu --action=clean --config=cpu2017-wllvm all
rm -rf benchspec/CPU/*/exe/
rm -rf benchspec/CPU/*/build/
rm -rf benchspec/CPU/*/run/
runcpu --action=build --tune=base --config=cpu2017-wllvm 500 502 505 508 510 511 519 520 523 525 526 531 538 541 544 557 600 602 605 619 620 623 625 631 638 641 644 657
```

--------------------------------

### Set Up SVF Environment (Debug)

Source: https://github.com/svf-tools/svf/wiki/User-Guide

Sets up the SVF environment variables for the debug version executables. Ensure you have built the debug version of SVF before running this command.

```bash
cd $SVF_HOME
. ./setup.sh debug
```

--------------------------------

### Extract Bitcode from RIOT ELF

Source: https://github.com/svf-tools/svf/wiki/Compile-bitcode-file-using-wllvm-gclang

After compiling the RIOT example, use get-bc to extract the bitcode file from the generated ELF executable.

```bash
cd bin/native/
get-bc default.elf
```

--------------------------------

### Fetch Chromium Source Code

Source: https://github.com/svf-tools/svf/wiki/Compiling-Chrome-using-flto

Create a directory for Chromium and fetch the source code using depot_tools. This command downloads the necessary files without running hooks initially.

```bash
$ mkdir ~/chromium
$ cd ~/chromium
$ fetch --nohooks chromium
$ cd src
```

--------------------------------

### Example: REALLOC_RET Annotation for Reallocation

Source: https://github.com/svf-tools/svf/wiki/Handling-External-APIs-with-extapi.c

Shows the REALLOC_RET annotation, used when a function reallocates memory and returns a pointer to the newly allocated object.

```c
__attribute__((annotate("REALLOC_RET")))
char *getcwd(char *buf, unsigned long size)
{
    return NULL;
}
```

--------------------------------

### Query Alias Results

Source: https://github.com/svf-tools/svf/wiki/A-simple-driver-example-of-SVF

An example function to query the alias results between two LLVM values using a given pointer analysis object.

```cpp
/*!
 * An example to query alias results of two LLVM values
 */
AliasResult aliasQuery(PointerAnalysis* pta, Value* v1, Value* v2){
	return pta->alias(v1,v2);
}

```

--------------------------------

### Pull SVF Docker Image

Source: https://github.com/svf-tools/svf/wiki/Setup-Guide

Download the latest SVF Docker image. This is useful for running SVF in an isolated environment without local installation.

```bash
docker pull svftools/svf:latest
docker run -it svftools/svf:latest /bin/bash
```

--------------------------------

### Configure and Build LLVM

Source: https://github.com/svf-tools/svf/wiki/Build-LLVM-and--Clang-from-source-code

Creates a build directory for LLVM and configures the build using CMake, then initiates the compilation process. Supports both release and debug builds.

```bash
mkdir llvm-16.0.0.obj
cd llvm-16.0.0.obj
cmake -DCMAKE_BUILD_TYPE=MinSizeRel ../llvm-16.0.0.src (or add "-DCMAKE_BUILD_TYPE:STRING=Debug" for debug version)
make -j8
```

--------------------------------

### Find Z3 Dependency

Source: https://github.com/svf-tools/svf/blob/master/CMakeLists.txt

Locates the Z3 theorem prover library using CMake's find_package command. It requires the Z3 package to be installed or discoverable.

```cmake
find_package(Z3 REQUIRED)
message(
  STATUS
    "Using Z3 package:
  Z3 major version:     ${Z3_VERSION_MAJOR}
  Z3 minor version:     ${Z3_VERSION_MINOR}
  Z3 patch version:     ${Z3_VERSION_PATCH}
  Z3 tweak version:     ${Z3_VERSION_TWEAK}
  Z3 version string:    ${Z3_VERSION_STRING}
  Z3 link libraries:    ${Z3_LIBRARIES}
  Z3 C include dirs:    ${Z3_C_INCLUDE_DIRS}
  Z3 C++ include dirs:  ${Z3_CXX_INCLUDE_DIRS}"
)
```

--------------------------------

### AddrStmt Example for malloc

Source: https://github.com/svf-tools/svf/wiki/Specifications-in-ExtAPI.json

Defines the 'malloc' function with its return type, arguments, and type as EFT_ALLOC. It specifies that the object created by malloc will be assigned to the return value.

```json
"malloc":   {
           "return":  "void *",
           "arguments":  "(size_t)",
           "type": "EFT_ALLOC",
           "overwrite_app_function": 1,
           "AddrStmt": {
            "src": "Obj",
            "dst": "Ret"
         }
       }
```

--------------------------------

### Print Points-to Set

Source: https://github.com/svf-tools/svf/wiki/A-simple-driver-example-of-SVF

An example function to print the points-to set of an LLVM value. It retrieves the node ID, the points-to set, and associated values from the PAG.

```cpp
/*!
 * An example to print points-to set of an LLVM value
 */
std::string printPts(PointerAnalysis* pta, Value* val){

    std::string str;
    raw_string_ostream rawstr(str);

    NodeID pNodeId = pta->getPAG()->getValueNode(val);
    NodeBS& pts = pta->getPts(pNodeId);
    for (NodeBS::iterator ii = pts.begin(), ie = pts.end();
            ii != ie; ii++) {
        rawstr << " " << *ii << " ";
        PAGNode* targetObj = pta->getPAG()->getPAGNode(*ii);
        if(targetObj->hasValue()){
            rawstr << "(" <<*targetObj->getValue() << ")\t ";
        }
    }

    return rawstr.str();

}

```

--------------------------------

### Map LLVM Components to Libraries

Source: https://github.com/svf-tools/svf/blob/master/svf-llvm/CMakeLists.txt

Uses llvm_map_components_to_libnames to get the correct library names for SVF. Excludes transitive SVF libraries from the host LLVM tree.

```cmake
if(LLVM_LINK_LLVM_DYLIB)
  set(LLVM_LIBRARIES LLVM)
else()
  llvm_map_components_to_libnames(LLVM_LIBRARIES
    analysis
    bitwriter
    core
    instcombine
    instrumentation
    ipo
    irreader
    linker
    scalaropts
    support
    target
    transformutils
    demangle
    Passes
  )
  # When the host LLVM tree already contains an in-tree SVF integration,
  # llvm_map_components_to_libnames() can pull in those LLVMSvf* libraries
  # transitively. Exclude them so the standalone SVF build links only against
  # its own SvfCore/SvfLLVM targets.
  list(FILTER LLVM_LIBRARIES EXCLUDE REGEX "^LLVMSvf(Core|LLVM)$|^LLVMSVFAnalysis$")
endif()
```

--------------------------------

### Clone and Build SVF

Source: https://github.com/svf-tools/svf/wiki/TypeClone

Clone the SVF repository and build the project. Ensure to check the 'Unit tests' section for ctir-related build options.

```bash
$ git clone https://github.com/SVF-tools/SVF
$ cd SVF
$ . build.sh  # See the 'Unit tests' section for info on ctir-related options.
```

--------------------------------

### Memset-like Statement Example

Source: https://github.com/svf-tools/svf/wiki/Specifications-in-ExtAPI.json

Specifies a side-effect similar to the `memset` function. It defines the source, destination, and size for memory operations, typically used for initializing memory blocks.

```json
"llvm.memset":  {
        "return":  "void",
        "arguments":  "(i8*, i8, i32, i32, i1)",
        "type": "EFT_L_A0__A0R_A1",
        "overwrite_app_function": 0,
        "memset_like":  {
            "src": "Arg0",
            "dst": "Arg1",
            "size": "Arg2"
        }
      }
```

--------------------------------

### Build Z3 Dynamic Library

Source: https://github.com/svf-tools/svf/wiki/Init-Z3-prover

Steps to build the Z3 dynamic library using the provided build scripts. Ensure you are in the cloned z3 directory before executing.

```bash
cd z3
python scripts/mk_make.py
cd build
make
sudo make install
```

--------------------------------

### Analyze CPU2006 Benchmarks with Gold-Plugin

Source: https://github.com/svf-tools/svf/wiki/Compiling-CPU2000-2006-2017

This command analyzes the CPU2006 benchmark suite to generate bc files using a specified configuration. Ensure you are in the $CPU2000_HOME directory and have sourced the shrc file.

```bash
cd $CPU2000_HOME
. ./shrc
rm -rf benchspec/CPU2006/*/exe/
runspec  --action=run --config=cpu2006-flto --tune=base --size=test --iterations=1 --noreportable all
```

--------------------------------

### Point-to Analysis Results File Format

Source: https://github.com/svf-tools/svf/wiki/SVF-Point‐to-Analysis-Results-Read-and-Write

This is an example of the structure of a point-to analysis results file generated by SVF. It includes sections for objVar, pts results, and GepObjVarMap.

```txt
// objVar of the target code. 
2 0
3 0
66 0
67 0
71 0
------
// the pts results of the target code.
0 -> {  }
1 -> {  }
2 -> { 3 }
74 -> { 3 5731 9799 13511 18277 }
------
// the GepObjVarMap of the target code.
10453 0 41965
10421 0 41964
9901 0 41959
31822 0 41958
31706 0 41957
------
// objVar of the target code. 
2 0
3 0
66 0
67 0
71 0

```

--------------------------------

### Configure Build Directory and Parallelism

Source: https://github.com/svf-tools/svf/wiki/Setup-SVF-in-CLion

Specify the build directory and the number of parallel jobs for the build process. Adjust '-j' based on your system's core count for optimal build times.

```bash
-j 12
```

--------------------------------

### Basic VSFS Invocation

Source: https://github.com/svf-tools/svf/wiki/VSFS

Use the `-vfspta` option to enable VSFS. Ensure `-opt-svfg` is set to `false` as versioning is not supported on optimized SVFGs.

```bash
$ wpa -vfspta -opt-svfg=false program.bc

```

--------------------------------

### Backup Binutils

Source: https://github.com/svf-tools/svf/wiki/Install-LLVM-Gold-Plugin-on-Ubuntu

Backs up the existing ar, nm, ld, and ranlib executables before replacing them.

```bash
cd ~
mkdir backup
cd /usr/bin/
cp ar ~/backup/
cp nm ~/backup/
cp ld ~/backup/
cp ranlib ~/backup/
```

--------------------------------

### Create CMake Package Configuration File

Source: https://github.com/svf-tools/svf/blob/master/CMakeLists.txt

Generates the main CMake configuration file (`SVFConfig.cmake`) used by `find_package(SVF)`. It requires a template file and specifies installation paths.

```cmake
configure_package_config_file(
  cmake/SVFConfig.cmake.in ${SVF_BINARY_DIR}/lib/cmake/SVF/SVFConfig.cmake
  INSTALL_DESTINATION ${SVF_INSTALL_CMAKECONFIGDIR}
  PATH_VARS SVF_INSTALL_BINDIR
            SVF_INSTALL_LIBDIR
            SVF_INSTALL_EXTAPIDIR
            SVF_INSTALL_EXTAPI_BC
            SVF_INSTALL_INCLUDEDIR
            SVF_INSTALL_PKGCONFDIR
            SVF_INSTALL_CMAKECONFIGDIR
)
```

--------------------------------

### Conditional Statement Example

Source: https://github.com/svf-tools/svf/wiki/Specifications-in-ExtAPI.json

Defines a conditional statement with true and false branches, each specifying a condition and a copy operation. Used when the behavior of an external function depends on the comparison of its arguments.

```json
{
           "return":  "void",
           "arguments":  "(char **, char **)",
           "type": "EFT_FREE_MULTILEVEL",
           "overwrite_app_function": 1,
           "CondStmt": {
               "TrueBranch": {
                   "Condition": "arg0 == arg1",
                   "CopyStmt": {
                       "src": "Arg0",
                       "dst": "Arg1"
                   }
               },
               "FalseBranch": {
                   "Condition": "arg0 != arg1",
                   "CopyStmt": {
                       "src": "Arg1",
                       "dst": "Ret"
                   }
              }
          }
      }
```

--------------------------------

### List Docker Images

Source: https://github.com/svf-tools/svf/wiki/Try-SVF-in-Docker

Display a list of all Docker images available on your system.

```bash
docker image ls
```

--------------------------------

### Create mozconfig File

Source: https://github.com/svf-tools/svf/wiki/Compiling-Firefox

Creates an empty 'mozconfig' file in the root directory of the Firefox source tree.

```bash
$ cd firefox-58.0b9
$ touch mozconfig
```

--------------------------------

### Analyze CPU2000 Benchmarks with Gold-Plugin

Source: https://github.com/svf-tools/svf/wiki/Compiling-CPU2000-2006-2017

This command analyzes the CPU2000 benchmark suite to generate bc files using a specified configuration. Ensure you are in the $CPU2000_HOME directory and have sourced the shrc file.

```bash
cd $CPU2000_HOME
. ./shrc
rm -rf benchspec/CINT2000/*/exe/
rm -rf benchspec/CFP2000/*/exe/
runspec  --action=run --config=cpu2000-flto --tune=base --size=test --iterations=1 --noreportable all
```

--------------------------------

### Configure LLVM Build with Gold Plugin

Source: https://github.com/svf-tools/svf/wiki/Install-LLVM-Gold-Plugin-on-Ubuntu

Configures the LLVM build, specifying the include directory for binutils and optionally setting the build type to Debug.

```bash
mkdir llvm-6.0.0.obj
cd llvm-6.0.0.obj
cmake ../llvm-6.0.0.src -DLLVM_BINUTILS_INCDIR="PATH_TO_binutils_SRC/include"
(or "cmake -D CMAKE_BUILD_TYPE:STRING=Debug ../llvm-6.0.0.src -DLLVM_BINUTILS_INCDIR="PATH_TO_binutils_SRC/include"" for debug version)
make -j8
```

--------------------------------

### Print Command to Run CPU2000 Benchmark Executable

Source: https://github.com/svf-tools/svf/wiki/Compiling-CPU2000-2006-2017

This command prints the specific command line needed to run an executable for a given benchmark. Navigate to the benchmark's run directory first.

```bash
cd benchspec/CINT2000/252.eon/run/00000001/
specinvoke -n
```

--------------------------------

### Run PTABen Test Cases

Source: https://github.com/svf-tools/svf/wiki/Try-SVF-in-Docker

Navigate to the PTABen directory and execute the test script for Andersen's analysis.

```bash
cd PTABen
./runtest.sh
```
Tokens:
Raw