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

This branch is 33 commits ahead of, 125 commits behind klee/klee:master.

Folders and files

NameName
Last commit message
Last commit date

Latest commit

28ec23d · Nov 9, 2023
Jun 7, 2023
Oct 25, 2023
Jun 5, 2023
Jun 5, 2023
Jul 30, 2019
Oct 25, 2023
Nov 9, 2023
Nov 6, 2023
Jun 11, 2023
Mar 23, 2023
Sep 11, 2023
Jul 21, 2023
Jul 10, 2023
Mar 17, 2023
Nov 6, 2023
Mar 17, 2023
Jun 5, 2023
May 26, 2023
Dec 19, 2019
Apr 9, 2015
May 26, 2017
Jun 7, 2023
Jun 7, 2023
Mar 3, 2015
Jun 7, 2023
Jun 7, 2023
Nov 7, 2023
Oct 25, 2023

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%