SeaDsa is a scalable, context-, field-, and array-sensitive points-to analysis tool for LLVM bitcode designed to enhance verification of low-level C/C++ programs.
A new context, field, and array-sensitive heap analysis for LLVM bitcode based on DSA.
SeaDsa is primarily used for precise heap analysis and points-to information extraction in LLVM bitcode, aiding program verification and security analysis of C/C++ applications. It is suitable for developers and researchers working on static analysis, program verification, and security automation who need detailed memory graph insights and integration with verification frameworks like SeaHorn.
SeaDsa requires LLVM 14 and Boost >= 1.65; users should ensure these dependencies are correctly installed. While it can analyze arbitrary LLVM bitcode, it is optimized for C/C++ verification tasks. Visualization of memory graphs requires additional Python packages and graphviz development libraries. Disabling compiler optimizations (-O0) is recommended for simple examples to preserve code structure for analysis.
Ensure C++ compiler supporting C++14 is installed
Install Boost library version 1.65 or higher
Install LLVM 14 and ensure LLVM header files and libraries are accessible
Clone the repository and navigate to its root directory
Create and enter a build directory: mkdir build && cd build
Run cmake with LLVM directory specified: cmake -DCMAKE_INSTALL_PREFIX=run -DLLVM_DIR=__here_llvm-14__/share/llvm/cmake ..
Build and install the tool: cmake --build . --target install
To run tests, install Python packages: pip install lit OutputCheck
Install additional Python packages: easy_install networkx pygraphviz
Install graphviz development libraries: sudo apt-get install libgraphviz-devclang -O0 -c -emit-llvm -S tests/c/simple.c -o simple.ll
Generate LLVM bitcode from a C source file with optimizations disabled for clearer analysis.
sea-dsa simple.ll
Run SeaDsa points-to analysis on the generated LLVM bitcode file.
cmake --build . --target test-sea-dsa
Run the SeaDsa test suite to verify the build and functionality.
include_directories(seadsa/include) and add_subdirectory(seadsa) in CMakeLists.txt
Integrate SeaDsa into other C++ projects using CMake for compilation and linking.