SVFIR

• SVFIR is the demo program sample to understand SVFIR and their graph representations, i.e., ICFG and PAG

SVFIR Layout

SVFIR/

|-- CMakeLists.txt
|-- SVFIR.cpp
`-- src
    |-- swap.c
    `-- example.c
    

1. Get the latest code template

* Before coding, please type cd $HOME/Teaching-Software-Verification and git pull in your terminal to make sure you always have the latest version of the code template.

2. LLVM IR Generation

* Use control + ~ to call out command line

Option 1: Generate LLVM IR of example.c via the following command line

cd /home/SVF-tools/Teaching-Software-Verification/CodeGraph
clang -S -c -O0 -fno-discard-value-names -emit-llvm src/example.c -o example.ll
opt -S -mem2reg example.ll -o example.ll

Option 2: Generate LLVM IR via compile.sh

cd /home/SVF-tools/Teaching-Software-Verification/SVFIR
sh compile.sh src/example.c

The two .ll file (i.e., example.ll) will be generated under the /home/SVF-tools/Teaching-Software-Verification/SVFIR folder

3. Run and Debug your SVFIR

3.1 launch.json

You need to set the "program" to be the executable file of SVFIR, i.e., "${workspaceFolder}/bin/svfir" in launch.json in order to run and debug

You need to set the "args" to be the .ll file you have just generated, i.e., "${workspaceFolder}/SVFIR/example.ll" in launch.json in order to run and debug

3.2 Click the run button

• The two dot files (i.e, example.ll.icfg.dot and example.ll.pag.dot) will be generated under the /home/SVF-tools/Teaching-Software-Verification/SVFIR folder

4. Visualize ICFG and SVFIR (PAG) graph

4.1 VSCode Graphviz Interactive Preview extensions

4.2 Open the dot file and graph visualization

• Open the dot file under, for example, /home/SVF-tools/Teaching-Software-Verification/SVFIR/example.ll.icfg.dot which is the ICFG of the program and call out the command palette

• Enter Graphviz and select `Interactive Preview (beside)

• You will see the ICFG on the right hand side