Skip to content
forked from klee/klee

Implement PDG AutoVectorization on KLEE Symbolic Execution Engine

License

Notifications You must be signed in to change notification settings

zhaosiying12138/klee

 
 

Repository files navigation

PDG AutoVectorization

A toy auto-vectoraization implementation about the application of Program Dependence Graph using LLVM by zhaosiying12138.
It can do auto-vectoraization when control flow exists since its If-Conversion algorithm can treat Control Dependence as Data Dependence.

1. File Organization

lib/Module/PDGAnalysis.cpp: an LLVM Analysis Pass to generate PDG information from LLVM IR;
lib/Module/Tarjan_SCC.cpp: an utility class to calculate SCC of PDG;
lib/Module/isl_ddg_analysis.c: an utility program to calculate Data Dependence Graph(DDG) to construct PDG, however, since I haven't integrate ISL into KLEE(我不会,斯米马赛~~), you need put this file into the ISL source code dictionary and compile, for more information please visit: https://github.com/zhaosiying12138/isl and 《零基础入门依赖环的检测》-流霞祭司曌鹓鶵;
lib/Core/PDGExecutor.cpp: modification on klee executor to executor loops of LLVM IR in a Loop-Distribution-Form automatically;
zsy_test/demo2_3.ll: the demo LLVM IR executed to test the overall algorithm;
zsy_test/demo3_3.ll: the demo LLVM IR executed to test CDG Construction algorithm only;
zsy_test/demo4.c: the demo C source code to show the principle of the PDG-AutoVec algorithm;

2. Usage

Step 1: Make a testfile (You can skip this step if you would like to use [zsy_test/demo2_3.ll] provided for you if you just want to learn the principle of PDG_AutoVec)

clang -Xclang -disable-O0-optnone -S -O0 -emit-llvm demo1.c -o demo1_1.ll  
opt -S -mem2reg demo1_1.ll -o demo1_2.ll  
opt -S -loop-simplify demo1_2.ll -o demo1_3.ll  

Step 2: Build modified KLEE

mkdir build  
cd build  
cmake .. -DCMAKE_BUILD_TYPE=Debug -DENABLE_SOLVER_Z3=ON -DZ3_INCLUDE_DIRS=/your-z3-dir/include/ -DZ3_LIBRARIES=/your-z3-dir/lib/libz3.so -DLLVM_DIR=/your-llvm-dir/  
make -j 65535  

Step 3: Execute the LLVM IR using KLEE

build/bin/klee zsy_test/demo2_3.ll  

3. Experimental Results

1. CDG Construction


2. DDG Construction

3. PDG Construction & Cut SCC & Toposort


4. KLEE Execution Result


5. Algorithm Extension when Exit Branch exits




4. Link

《零基础入门控制依赖图构建的理论与实践》-流霞祭司曌鹓鶵
《零基础入门基于程序依赖图对带有控制流程序自动向量化的实现》-流霞祭司曌鹓鶵

5. Copyright

Copyright (c) 2023 By 流月城先进偃甲技术研究院-对伏羲外包国家重点实验室-流霞祭司曌鹓鶵 founded by 五色石炼制关键工艺天界自然科学基金(2022LYC12138). All rights reserved.

About

Implement PDG AutoVectorization on KLEE Symbolic Execution Engine

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Languages

  • C++ 66.9%
  • C 18.2%
  • LLVM 5.9%
  • Python 3.7%
  • CMake 3.3%
  • Shell 1.1%
  • Other 0.9%