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.

Sometimes tutors may request pull the latest docker images, just follow the document Installation-of-Docker.

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/SVFIR
clang -S -c -O0 -fno-discard-value-names -emit-llvm src/example.c -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 .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