Skip to content

SVFG Read and Write

Yulei Sui edited this page Feb 8, 2022 · 2 revisions

Introduction

The aim of SVFG read and write is to implement functions that will write a SVFG to a file and then read the SVFG back into memory from a file.

Code location

The two functions (writeToFile and readFile) are located at SVFG.cpp / SVFG.h

The current implementation is located in lukekoko's fork, under the branch SVFG-rw.

Pull request: PR

Text file format

The outputted SVFG will be in the follow file format. First the SVFG nodes are written.

\_\_Nodes\_\_

SVFGNodeID: <id> >= <node type> >= MVER: {MRVERID: <id> MemRegion: pts{<pts> } MRVERSION: <version> MSSADef: <version>, pts{<pts> }} >= ICFGNodeID: <id>

After the SVFG nodes are written, the SVFG edges are written.

\_\_Edges\_\_

srcSVFGNodeID: <id> => dstSVFGNodeID: <id> >= <edge type> | MVER: {MRVERID: <id> MemRegion: pts{<pts> } MRVERSION: <version> MSSADef: <version>, pts{<pts> }}

Testing

To test we are using the diff test cases in the Test-Suite. The following lines in CMakeLists.txt are the testcases for SVFG. SVFG testcases. We are also testing on crux-bc files Crux bc testcases.

The current implementation is failing on the crux-bc dc.bc file. (Link to CI/CD failing test).

To test locally using the Test-suite.

  1. Clone the Test-Suite into the root of SVF
  2. Run ./build.sh debug
  3. cd into Debug-build
  4. Run ctest

VSCode settings for debugging

The following configuration is for running a SVFG write and read using VSCode's debugging.

{
    "name": "svfg write to file",
    "type": "cppdbg",
    "request": "launch",
    "program": "${workspaceFolder}/Debug-build/bin/wpa",
    "args": ["-fspta", "--write-svfg=svf.txt", "../../Test-Suite/test_cases_bc/crux-bc/dc.bc"],
    "stopAtEntry": false,
    "cwd": "${workspaceFolder}/Debug-build/bin",
    "environment": [],
    "externalConsole": false,
    "MIMode": "gdb",
    "setupCommands": [
        {
            "description": "Enable pretty-printing for gdb",
            "text": "-enable-pretty-printing",
            "ignoreFailures": true
        }
    ]
},
{
    "name": "svfg read file",
    "type": "cppdbg",
    "request": "launch",
    "program": "${workspaceFolder}/Debug-build/bin/wpa",
    "args": ["-fspta", "--read-svfg=svf.txt", "../../Test-Suite/test_cases_bc/crux-bc/dc.bc"],
    "stopAtEntry": false,
    "cwd": "${workspaceFolder}/Debug-build/bin",
    "environment": [],
    "externalConsole": false,
    "MIMode": "gdb",
    "setupCommands": [
        {
            "description": "Enable pretty-printing for gdb",
            "text": "-enable-pretty-printing",
            "ignoreFailures": true
        }
    ]
},