ماشین مجازی نمادین[1] KLEE بر فراز زیرساخت گردآورنده LLVM ساخته شده[2] است و در حال حاضر دو بخش اصلی وجود دارد:

هسته موتور ماشین مجازی نمادین که مسئول اجرای ماژول های بیتکد[3] LLVM با پشتیبانی از مقدارهای نمادین است. این بخش از کدهای موجود در مسیر lib تشکیل شده است.
لایه شبیه سازی[4] POSIX و لینوکس که برای پشتیبانی از uClibc ساماندهی شده است و پشتیبانی بیشتری برای نمادین کردن بخش هایی از محیط سامانه عامل فراهم می کند.

افزون بر این یک کتابخانه ساده برای بازاجرای داده های ورودی محاسبه شده بر روی کد بومی برنامه‌های بسته وجود دارد. همچنین یک زیرساخت پیچیده تر برای بازاجرای داده‌های ورودی تولیدشده برای لایه شبیه سازی POSIXو لینوکس فراهم شده است که اجرای برنامه‌های بومی را در محیطی سازگار با داده آزمایشی محاسبه شده پردازش می کند، از جمله راه اندازی پرونده‌ها، لوله‌ها، متغیرهای محیطی و سپردن آرگومان‌های خط فرمان به برنامه.

1. مراحل نصب

توجه داشته باشید آخرین ریلیز رسمی با llvm-13 سازگار است و می‌‍توانید مطابق با این مستندات آن را نصب و راه اندازی نمایید ما در ادامه نسخه منتشر نشده که با llvm-16 سازگار است را نصب می‌کنیم.

بر اساس این لینک، نصب klee به سه روش زیر امکان پذیر است:

1.1 1- توسط داکر:

در صورتی که روی سیستم داکر را نصب ندارید می توانید آن را از طریق این لینک نصب کنید.

نصب آخرین نسخه موجود klee با داکر به روش زیر است:

				
					docker pull klee/klee

نصب داکر ایمج به صورت لوکال به روش زیر است:

				
					$ git clone https://github.com/klee/klee.git
$ cd klee
$ docker build -t klee/klee .

برای اطلاعات بیشتر این لینک مراجعه کنید.

1.2 2- از طریق Package Manager:

برای نصب کردن klee روی سیستم‌های Fedora, Debian و سایر توزیع‌های اصلی لینوکس به روش زیر است:

				
					sudo apt update
sudo apt install snapd
sudo snap install klee

1.3 3- نصب به صورت دستی:

1. ساخت از منبع بر پایه LLVM 16: این نسخه در حال حاضر توصیه شده است.
2. ساخت پیکربندی های دلخواه KLEE: برای ساخت پیکربندی‌های مختلف KLEE و وابستگی های آن.

				
					sudo apt update
sudo apt install llvm-13 clang-13

در ادامه، مراحل روش ساخت از منبع بر پایه LLVM 16 توضیح داده شده است:

1- نصب پیش نیازها:

KLEE به تمامی وابستگی‌های LLVM نیاز دارد (رجوع شود به اینجا) و همچنین به برخی وابستگی‌های دیگر.

به طور خاص، باید برنامه ها و کتابخانه های فهرست شده در ادامه را نصب کنید. graphviz و doxygen اختیاری هستند و تنها برای تولید مستندات کد منبع لازم می‌باشند.

در اوبونتو، از دستور زیر استفاده کنید:

				
					$ sudo apt-get install build-essential cmake curl file g++-multilib gcc-multilib git libcap-dev libgoogle-perftools-dev libncurses-dev libsqlite3-dev libtcmalloc-minimal4 python3-pip unzip graphviz doxygen

در macOS، دستور زیر را اجرا کنید:

				
					$ brew install curl git cmake python unzip gperftools sqlite3 graphviz doxygen bash

همچنین باید lit را برای فعال کردن آزمون‌ها، tabulate را برای پشتیبانی از ویژگی‌های اضافی در klee-stats و wllvm را برای ساده‌تر کردن کامپایل برنامه‌ها به بیتکد (bitcode) LLVM نصب کنید:

				
					$ sudo apt-get install pipx
$ pipx install lit
$ pipx install wllvm

در توزیع‌های قدیمی‌تر اوبونتو، ممکن است به جای آن نیاز باشد از دستور زیر استفاده کنید:

				
					$ sudo pip3 install lit wllvm
$ sudo apt-get install python3-tabulate

اطمینان حاصل کنید که مسیرهایی مانند ~/.local/bin (با دستور python3 -m site –user-base در سیستم خود بررسی کنید) در متغیر PATH شما قرار دارند.

2. نصب LLVM 16 :KLEE بر فراز LLVM ساخته می شود؛ نخستین گام ها به دست آوردن یک نصب کارای LLVM است. برای اطلاعات بیشتر به راهنمای Getting Started with the LLVM System مراجعه کنید.

اگر از اوبونتو تازه (برای نمونه 24.04) یا دبیان استفاده می کنید، توصیه می شود از بسته های LLVM که توسط خود LLVM از طریق نشانی apt.llvm.org ارائه می‌شوند استفاده کنید.

مخازن مربوط به توزیع خود را به پرونده ‎/etc/apt/sources.list بیفزایید و سپس کلید آن ها را وارد کنید:

				
					$ wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key|sudo apt-key add -

اکنون باید قادر باشید LLVM را نصب کنید:

				
					$ sudo apt-get install clang-16 llvm-16 llvm-16-dev llvm-16-tools

مراحل زیر را در ubuntu 22.04 دنبال کنید:

				
					get https://apt.llvm.org/llvm.sh
chmod u+x llvm.sh
sudo ./llvm.sh 16

sudo mkdir -p /etc/apt/keyrings
sudo mv /etc/apt/trusted.gpg.d/apt.llvm.org.asc /etc/apt/keyrings/

sudo nano /etc/apt/sources.list.d/archive_uri-http_apt_llvm_org_noble_.list
add below text:
[arch=amd64 signed-by=/etc/apt/keyrings/apt.llvm.org.asc]

sudo apt update

sudo apt install clang-16 lldb-16 lld-16 clangd-16

اگر از macOS استفاده می کنید، می توانید بسته های قدیمی‌تر LLVM را با استفاده از brew نصب کنید:

				
					$ brew install llvm@16

همین برای LLVM کافی است. اگر می خواهید آن را به صورت دستی نصب کنید، به مستند رسمی LLVM Getting Started مراجعه کنید.

3- نصب حلگرهای قیود (constraint solver):

KLEE از چندین حلگر قید پشتیبانی می کند. برای ساخت KLEE باید دست کم یکی از آن ها را نصب کنید.

STP به طور تاریخی KLEE بر پایه STP ساخته شده است، بنابراین پشتیبانی از این حلگر پایدارترین حالت را دارد. برای دستورهای ساخت، به اینجا مراجعه کنید.
Z3 حلگر دیگری است که KLEE از آن پشتیبانی می کند و از پایداری مناسبی برخوردار است. باید از نسخه 4.4 یا بالاتر Z3 استفاده کنید. Z3 در بسیاری از توزیع ها بسته بندی شده است. برای دستورهای ساخت، به اینجا مراجعه کنید.
metaSMT از حلگرهای گوناگونی پشتیبانی می کند، از جمله Boolector ،CVC4 ،STP ،Z3 و Yices. شاخه rc1 پیشنهاد می شود (git clone -b v4.rc1 …). برای دستورهای ساخت، به اینجا مراجعه کنید.

نصب stp:

				
					#install deps
sudo apt-get update
sudo apt-get install -y \
    libgmp-dev \
    libgmpxx4ldbl \
    pkg-config \
    libboost-all-dev
sudo apt-get install -y libboost-program-options-dev
sudo apt-get install git cmake bison flex libboost-all-dev libgmp-dev python2 perl
git clone https://github.com/stp/stp
cd stp
git checkout 2.3.4_cadical
git submodule init &amp;&amp; git submodule update
./scripts/deps/setup-gtest.sh
./scripts/deps/setup-outputcheck.sh
./scripts/deps/setup-cms.sh
./scripts/deps/setup-minisat.sh
mkdir build
cd build
cmake ..
cmake --build .
sudo cmake --install .

echo 'ulimit -s unlimited' &gt;&gt; ~/.bashrc
echo 'export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:/home/test/stp/deps/install/lib' &gt;&gt; ~/.bashrc
source ~/.bashrc

نکته مهم:

				
					we must patch CMakeLists.txt

original

# -----------------------------------------------------------------------------
# Setup Cadical
# -----------------------------------------------------------------------------
option(USE_CADICAL "Try to use Cadical" ON)
add_feature_info(Cadical USE_CADICAL "Enables Cadical solver")

if (USE_CADICAL)
    set(CADICAL_DIR "/home/thansen/solvers/cadical" CACHE PATH "Path to directory")
    add_definitions(-DUSE_CADICAL)
    include_directories(${CADICAL_DIR}/)        # should point to the base directory: ~/git/cadical/
    link_libraries(${CADICAL_DIR}/build/libcadical.a)  
endif()

change to:

# -----------------------------------------------------------------------------
# Setup Cadical (patched to use internal deps/cadical)
# -----------------------------------------------------------------------------
option(USE_CADICAL "Use bundled CaDiCaL" ON)
add_feature_info(Cadical USE_CADICAL "Enables Cadical solver")

if (USE_CADICAL)
    set(CADICAL_DIR "${PROJECT_SOURCE_DIR}/deps/cadical")

    add_definitions(-DUSE_CADICAL)

    # Include CaDiCaL headers
    include_directories(
        ${CADICAL_DIR} 
        ${CADICAL_DIR}/src 
        ${CADICAL_DIR}/build 
    )

    # Build CaDiCaL if static lib does not exist
    if (NOT EXISTS "${CADICAL_DIR}/build/libcadical.a")
        message(STATUS "Building bundled CaDiCaL...")
        execute_process(
            COMMAND make -j
            WORKING_DIRECTORY ${CADICAL_DIR}
        )
    endif()

    # Link the CaDiCaL static library
    link_libraries(${CADICAL_DIR}/build/libcadical.a)
endif()

در صورتی که نصب با موفقیت انجام شود خروجی مشابه زیر خواهد بود:

نصب z3:

				
					  pip install z3-solver

4- (اختیاری) دریافت کدهای منبع Google Test:

برای آزمون‌های واحد از کتابخانه های Google Test استفاده می کنیم. اگر می‌خواهید آزمون های واحد را اجرا کنید باید این گام را انجام دهید و همچنین هنگام پیکربندی KLEE در گام 8 گزینه ‎-DENABLE_UNIT_TESTS=ON را به CMake بدهید.

در حال حاضر نسخه 1.16.0 توصیه می شود، بنابراین کدهای منبع این نسخه را دریافت کنید.

				
					$ curl -OL https://github.com/google/googletest/archive/refs/tags/v1.16.0.zip
$ unzip v1.16.0.zip

این کار شاخه ای به نام googletest-1.16.0 می سازد.

5- (اختیاری) ساخت uClibc و مدل محیط POSIX (در macOS پشتیبانی نمی شود):

به طور پیش فرض KLEE روی برنامه های بسته کار می کند (برنامه هایی که از هیچ کد بیرونی مانند توابع کتابخانه C استفاده نمی کنند) اما اگر می خواهید از KLEE برای اجرای برنامه های واقعی استفاده کنید، باید زمان اجرای POSIX در KLEE را فعال کنید که بر فراز کتابخانه C مربوط به uClibc ساخته می شود.

				
					$ git clone https://github.com/klee/klee-uclibc.git
$ cd klee-uclibc
$ ./configure --make-llvm-lib # --with-cc clang-16 --with-llvm-config llvm-config-16
$ make -j
$ cd ..

هنگامی که clang یا llvm-config در متغیر محیطی PATH قرار نداشته باشند، یا دارای prefix/suffix سفارشی باشند، ممکن است اسکریپت configure قادر به شناسایی خودکار مسیر آن‌ها نباشد.

برای تعیین دستی مسیر این ابزارها، می‌توانید از گزینه‌های زیر استفاده کنید:

				
					--with-cc=
--with-llvm-config=

نکته:

اگر پلتفرم هدف شما معماری i386 یا x64 نباشد، لازم است ابتدا دستور make config را اجرا کرده و target صحیح را انتخاب کنید. مقادیر پیش‌فرض سایر متغیرهای uClibc معمولاً مناسب هستند.

برای آن‌که به KLEE اعلام کنید از klee-uclibc و POSIX runtime به‌طور هم‌زمان استفاده کند، هنگام اجرای CMake در مرحله ۸، گزینه‌های زیر را اضافه کنید:

				
					DENABLE_POSIX_RUNTIME=ON
DKLEE_UCLIBC_PATH=

که در آن، مقدار <KLEE_UCLIBC_SOURCE_DIR> مسیر مطلق دایرکتوری است که مخزن klee-uclibc در آن clone شده است.

6- گرفتن سورس KLEE:

				
					$ git clone https://github.com/klee/klee.git

7- (اختیاری) — ساخت ++libc:

برای اینکه بتوانید کدهای ++C را اجرا کنید، لازم است پشتیبانی از کتابخانه استاندارد ++C را نیز فعال نمایید.

اطمینان حاصل کنید که clang++-16 در مسیر (PATH) سیستم شما قرار دارد. سپس، از دایرکتوری اصلی (root) سورس KLEE، دستورهای زیر را اجرا کنید:

				
					$ LLVM_VERSION=16 BASE= ENABLE_OPTIMIZED=1 DISABLE_ASSERTIONS=1 ENABLE_DEBUG=0 REQUIRES_RTTI=1 scripts/build/build.sh libcxx

در اینجا، مقدار <LIBCXX_DIR> مسیر مطلق (absolute path) دایرکتوری است که قرار است ++libc در آن clone و build شود. برای اینکه به KLEE اعلام کنید از ++libc استفاده کند، هنگام اجرای CMake در مرحله ۸ باید گزینه‌های زیر را اضافه کنید:

				
					-DENABLE_KLEE_LIBCXX=ON
-DKLEE_LIBCXX_DIR=/libc++-install-160/
-DKLEE_LIBCXX_INCLUDE_DIR=/libc++-install-160/include/c++/v1/

برای فعال‌سازی پشتیبانی KLEE از Exception Handling در ++C نیز باید هنگام پیکربندی KLEE در مرحله ۸، گزینه‌های زیر را اضافه کنید:

				
					-DENABLE_KLEE_EH_CXX=ON
-DKLEE_LIBCXXABI_SRC_DIR=/llvm-160/libcxxabi/

توجه داشته باشید که مقدار <LIBCXX_DIR> باید حتماً یک مسیر مطلق باشد. اگر می‌خواهید ++libc را در مسیر home خود بسازید، توجه کنید که در برخی محیط‌ها (مانند Ubuntu 18.04)، علامت ~ ممکن است مسیر مطلق محسوب نشود. در چنین مواردی می‌توانید از متغیر محیطی HOME$ استفاده کنید.

8- پیکربندی KLEE:

باید KLEE را به‌صورت «خارج از سورس» (out-of-source build) کامپایل کنید.

بنابراین ابتدا لازم است یک دایرکتوری build ایجاد کنید.

این دایرکتوری می‌تواند در هر مسیری که می‌خواهید ایجاد شود.

در مثال‌های زیر، فرض بر این است که این دایرکتوری را داخل مخزن (repository) مربوط به KLEE ایجاد می‌کنید.

				
					mkdir build

حالا وارد (cd) دایرکتوری build شوید و CMake را برای پیکربندی KLEE اجرا کنید؛ که در آن <KLEE_SRC_DIRECTORY> مسیری است که مخزن (repository) مربوط به KLEE را در مرحله قبل clone کرده‌اید.

				
					$ cd build
$ cmake

گزینه‌های <CMAKE_OPTIONS> گزینه‌های پیکربندی هستند. این گزینه‌ها در فایل README-CMake.md مستند شده‌اند. برای مثال، اگر بخواهید KLEE را همراه با STP، POSIX runtime، klee-uclibc و unit testing بسازید، خط فرمان تقریباً به این صورت خواهد بود:

				
					$ cmake -DENABLE_SOLVER_STP=ON -DENABLE_POSIX_RUNTIME=ON -DKLEE_UCLIBC_PATH= -DENABLE_UNIT_TESTS=ON -DGTEST_SRC_DIR=

که در آن <KLEE_UCLIBC_SOURCE_DIR> مسیر مطلق درخت سورس klee-uclibc است و <GTEST_SOURCE_DIR> مسیر مطلق درخت سورس Google Test می‌باشد. یا به‌طور مشخص‌تر، با فرض اینکه src/ دایرکتوری کاری، /src/klee/build دایرکتوری build، و پشتیبانی ++libc فعال باشد:

				
					$ cmake -DENABLE_SOLVER_STP=ON -DENABLE_POSIX_RUNTIME=ON -DKLEE_UCLIBC_PATH=/src/klee-uclibc -DENABLE_UNIT_TESTS=ON -DGTEST_SRC_DIR=/src/googletest-1.16.0/ -DENABLE_KLEE_LIBCXX=ON -DKLEE_LIBCXX_DIR=/src/libcxx/libc++-install-160/ -DKLEE_LIBCXX_INCLUDE_DIR=/src/libcxx/libc++-install-160/include/c++/v1/ -DENABLE_KLEE_EH_CXX=ON -DKLEE_LIBCXXABI_SRC_DIR=/src/libcxx/llvm-160/libcxxabi/ ..

نکته ۱: می‌توانید تنها با تایپ کردن ..cmake از گزینه‌های پیش‌فرض KLEE استفاده کنید، اما این گزینه‌های پیش‌فرض شامل پشتیبانی uClibc و POSIX runtime نخواهند بود.

نکته ۲: اگر LLVM پیدا نشود یا لازم باشد نسخه خاصی استفاده شود، می‌توانید -DLLVM_DIR=<LLVM_DIR> را به CMake بدهید؛ که در آن <LLVM_DIR> مسیر مطلق دایرکتوری build یا نصب مرتبط است (برای مثال ‎/usr/lib/llvm-16/‎). به همین ترتیب، KLEE به یک کامپایلر C و ++C نیاز دارد که بتواند bitcode سازگار با نسخه LLVM مورد استفاده KLEE ایجاد کند. اگر این کامپایلرها به‌طور خودکار شناسایی نشوند، می‌توانید <DLLVMCC=<PATH_TO_CLANG و <DLLVMCXX=<++PATH_TO_CLANG را برای تعیین صریح این کامپایلرها پاس دهید؛ که در آن <PATH_TO_CLANG> مسیر مطلق clang و <++PATH_TO_CLANG> مسیر مطلق ++clang است.

نکته ۳: به‌طور پیش‌فرض، KLEE برای تخصیص حافظه از tcmalloc استفاده می‌کند تا گزارش مصرف حافظه بالاتر از ۲ گیگابایت پشتیبانی شود. اگر نمی‌خواهید tcmalloc (پکیج‌های Ubuntu شامل libtcmalloc-minimal4 و libgoogle-perftools-dev) را نصب کنید یا ترجیح می‌دهید از allocator مربوط به glibc استفاده کنید، هنگام پیکربندی KLEE گزینه -DENABLE_TCMALLOC=OFF را به CMake بدهید.

9- ساخت klee را از دایرکتوری build که در مرحله قبل ایجاد کردید، اجرا کنید:

				
					$ make

10- (اختیاری) اجرای مجموعه اصلی آزمون‌های رگرسیون:

اگر KLEE با فعال‌سازی آزمون‌های سیستمی پیکربندی شده باشد، می‌توانید آن‌ها را با دستور زیر اجرا کنید:

				
					$ make systemtests

اگر می‌خواهید lit را به‌صورت دستی فراخوانی کنید، از این دستور استفاده کنید:

				
					$ lit test/

به این روش می‌توانید آزمون‌های منفرد یا زیربخشی از مجموعه را اجرا کنید:

				
					$ lit test/regression

11- (اختیاری) ساخت و اجرای آزمون‌های واحد:

اگر KLEE با فعال‌سازی آزمون‌های واحد پیکربندی شده باشد، می‌توانید آزمون‌های واحد را بسازید و اجرا کنید:

				
					$ make unittests

نکته: می‌توانید هر دو، یعنی آزمون‌های سیستمی و آزمون‌های واحد را با دستور make check اجرا کنید.

12- شما آماده‌اید! برای استفاده از KLEE صفحه Documentation را بررسی کنید.

نکته: برای آزمون برنامه‌های واقعی (برای مثال Coreutils)، ممکن است لازم باشد محدودیت تعداد فایل‌های باز سیستم خود را افزایش دهید (ulimit -n). مقداری بین 10000 تا 999999 باید قابل‌قبول باشد. در بیشتر موارد، ابتدا لازم است محدودیت سخت (hard limit) افزایش داده شود، بنابراین بهتر است مستقیماً فایل پیکربندی مربوطه را ویرایش کنید (برای مثال /etc/security/limits.conf).

یک نمونه از کامپایل آسان klee به شکل زیر است.

				
					cd ./klee-build/klee
rm -rf build
mkdir build &amp;&amp; cd build
cmake -DENABLE_SOLVER_STP=ON -DENABLE_POSIX_RUNTIME=ON -DKLEE_UCLIBC_PATH=/home/test/klee-uclibc -DENABLE_UNIT_TESTS=ON -DGTEST_SRC_DIR=/home/test/googletest-1.16.0/ -DENABLE_KLEE_LIBCXX=ON -DKLEE_LIBCXX_DIR=/home/test/klee-build/klee-uclibc/libc++-install-160/ -DKLEE_LIBCXX_INCLUDE_DIR=/home/test/klee-build/klee-uclibc/libc++-build-160/include/c++/v1/ -DENABLE_KLEE_EH_CXX=ON -DKLEE_LIBCXXABI_SRC_DIR=/home/test/klee-build/klee-uclibc/llvm-160/libcxxabi/ .. 
make -j
make systemtests
lit test/
make unittests
make check
sudo cmake --install .

پس از نصب برای اطمینان از اجرای صحیح دستور زیر را اجرا کنید:

				
					klee –version

خروجی مشابه تصویر زیر خواهد بود:

2. نحوه استفاده از Klee

همانطور که در مرحله قبل ذکر شد در صفحه https://klee-se.org/docs میتوانید راهنما و مستندات کاربری klee را ببینید در این بخش ما صرفا “نحوه استفاده (Usage)” و ” آموزش‌ها (Tutorials)” را مورد بررسی قرار میدهیم تا با نحوه کار با این ابزار آشنا شویم.

2.1 نحوه استفاده

Intrinsics: مرور کلی بر توابع اصلی intrinsic در KLEE. در ادامه در بخش ” مروری بر توابع اصلی intrinsic در KLEE” این مورد را بررسی خواهیم کرد.
KLEE Options: مرور کلی بر گزینه‌های اصلی خط فرمان KLEE.
Generated Files: مرور کلی بر فایل‌های اصلی تولید شده توسط KLEE.
Tools: مرور کلی بر ابزارهای کمکی اصلی ارائه شده توسط KLEE.
Solver Chain: مرور کلی بر زنجیره solver و آرگومان‌های مربوط به خط فرمان آن.
Kleaver Options: مرور کلی بر گزینه‌های اصلی خط فرمان Kleaver.
KQuery: راهنمای مرجع برای زبان KQuery که برای تعامل با Kleaver استفاده می‌شود.
Coreutils Experiments: اطلاعاتی درباره آزمایش‌های Coreutils که در مقاله KLEE OSDI’08 ارائه شده‌اند.

در ادامه مورد اول را بررسی خواهیم کرد (موارد دیگر را می توانید با مراجعه به سایت https://klee-se.org/docs مورد مطالعه و بررسی قرار دهید):

2.2 مروری بر توابع اصلی intrinsic در KLEE

KLEE مجموعه‌ای از توابع ویژه فراهم می‌کند که در زمینه اجرای نمادین (symbolic execution) مفید هستند. هرگاه برنامه‌ای یکی از این توابع را فراخوانی کند، KLEE به‌صورت داخلی آن فراخوانی را مدیریت می‌کند و به همین دلیل، این توابع ماهیت intrinsic دارند و در فایل include/klee/klee.h اعلام شده‌اند.

مهم‌ترین و پرکاربردترین intrinsic، تابع klee_make_symbolic است که یک آبجکت نمادین بدون محدودیت (unconstrained symbolic object) ایجاد می‌کند.

2.2.1 klee_assume(condition)

2.2.1.1 نحوه استفاده

تابع klee_assume(condition)` برای محدود کردن مقادیری که متغیرهای نمادین می‌توانند داشته باشند استفاده می‌شود. اجرای باقیمانده برنامه تنها مقادیری از متغیرها را در نظر می‌گیرد که شرط `condition` را برآورده کنند.

از نظر مفهومی، klee_assume(condition)` معادل این است که باقی برنامه را در یک بلوک `if(condition){ }` قرار دهید، با این تفاوت که اگر شرط قابل‌برآورده شدن نباشد، `klee_assume` یک خطا چاپ می‌کند. از لحاظ فنی، klee_assume(condition)` شرط داده ‌شده را به محدودیت‌های مسیر جاری (current path constraints) اضافه می‌کند.

2.2.1.2 تعامل با عملگرهای کوتاه‌مدار (short-circuit operators)

هنگامی که شرط `condition` شامل عملگرهای کوتاه‌مدار باشد، نتایج intrinsic `klee_assume` ممکن است غیرمنتظره باشند. به عنوان مثال، کد زیر و خروجی مربوطه در KLEE نشان داده می‌شود:

				
					#include "klee/klee.h"

int main() {
  int c,d;
  klee_make_symbolic(&amp;c, sizeof(c), "c");
  klee_make_symbolic(&amp;d, sizeof(d), "d");

  klee_assume((c==2) &amp;&amp; (d==3));

  return 0;
}

				
					$ clang -O0 -I klee_path/include/ -g -c -emit-llvm p.c -o p.bc
$ klee p.bc
KLEE: output directory is "/path/klee-out-0"
KLEE: Using STP solver backend
KLEE: ERROR: /path/p.c:8: invalid klee_assume call (provably false)
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 23
KLEE: done: completed paths = 2
KLEE: done: generated tests = 2

ممکن است انتظار داشته باشید که برنامه تنها یک مسیر را طی کند، در حالی که KLEE دو مسیر پیدا می‌کند. دلیل این رفتار در نحوه مدیریت عملگرهای کوتاه‌مدار توسط کامپایلرها نهفته است. هنگام کامپایل، کد فوق به LLVM bitcode تبدیل می‌شود که مشابه کد C زیر است:

				
					#include "klee/klee.h"

int main() {
  int c,d;
  klee_make_symbolic(&amp;c, sizeof(c), "c");
  klee_make_symbolic(&amp;d, sizeof(d), "d");
  
  int tmp;
  if (c == 2) 
    tmp = d == 3;
  else
    tmp = 0;

  klee_assume(tmp);

  return 0;
}

از آنجا که برنامه شامل دو مسیر است و هر دو مسیر قابل اجرا هستند، klee_assume دو بار فراخوانی می‌شود: یک بار با عبارت مقایسه‌ای “d == 3” و یک بار با آرگومان ثابت ساده “0”. از آنجا که “0” معادل false است و هیچ مسیری نمی‌تواند این شرط را برآورده کند، KLEE یک پیام خطا چاپ می‌کند و مسیر مربوطه را خاتمه می‌دهد.

بهینه‌سازی‌های تهاجمی ‌تر (مثل Os-)، برنامه را به یک مسیر کاهش می‌دهند و klee_assume تنها یک بار با عبارت “c == 2 && d == 3” همان‌طور که انتظار می‌رود، فراخوانی می‌شود. توجه داشته باشید که موتورهای اجرای نمادین از عبارات (expressions) به‌ صورت داخلی برای نمایش محاسبات روی متغیرهای نمادین استفاده می‌کنند، اما رابط C تابع klee_assume همچنان نیازمند یک شرط بولی است.

به‌طور جانبی، امکان دستیابی به رفتار «یک مسیر» با جایگزینی عملگرهای منطقی && و || با نسخه‌های bitwise وجود دارد. برای انجام صحیح این کار، مطمئن شوید که تمام عملوندها مقادیر بولی دارند و هیچ اثر جانبی (side effect) ایجاد نمی ‌کنند.

نکته: خروجی فوق پس از کامپایل با Clang 6 به‌دست آمده است. سایر کامپایلرها یا نسخه‌ها ممکن است نتایج کمی متفاوت ارائه دهند.

2.2.2 klee_prefer_cex(object, condition)

این تابع به KLEE می‌گوید که هنگام تولید تست کیس‌ها به‌عنوان خروجی، برخی مقادیر را ترجیح دهد. یک state در KLEE می‌تواند با بسیاری از تست کیس‌های ممکن متفاوت متناظر باشد. برای مثال، در این کد:

				
					char input[4];
klee_make_symbolic(input, sizeof(input), "input");
assert(input[0] == 'Q');

KLEE یک state شکست‌خورده خواهد داشت که متناظر با `input = “aaaa”`، `input = “1234”` و هر ورودی دیگری است که شرط assert را نقض می‌کند. به‌طور معمول، هنگامی که KLEE برای این شکست یک تست کیس تولید می‌کند، می‌تواند هر یک از این ورودی‌های معتبر را انتخاب کند. نتیجه می‌تواند `input = “\0\0\0\0″` یا `input = “\xff\xff\xff\xff”` یا هر مقدار دیگر غیرقابل‌خواندن باشد. با استفاده از klee_prefer_cex` پس از `klee_make_symbolic` می‌توان آن را قابل‌خواندن‌تر کرد:

				
					for (int i = 0; i &lt; 4; i++)
  klee_prefer_cex(input, 32 &lt;= input[i] &amp;&amp; input[i] &lt;= 126); // assume ASCII

نکته: klee_prefer_cex` تنها باید بلافاصله پس از فراخوانی `klee_make_symbolic` استفاده شود و در حال حاضر پس از `klee_range` قابل استفاده نیست.

اکنون، هنگامی که KLEE بین بسیاری از تست کیس‌های ممکن انتخاب می‌کند، ترجیح می‌دهد از کاراکترهای قابل‌چاپ استفاده کند. وقتی KLEE مسیرهایی پیدا می‌کند که با شرط `klee_prefer_cex` مغایرت دارند، ترجیح را نادیده گرفته و تست کیس‌های احتمالا غیرقابل‌خواندن تولید می‌کند.

POSIX runtime به‌صورت داخلی از `klee_prefer_cex` استفاده می‌کند، به‌ویژه برای ترجیح دادن کاراکترهای قابل‌چاپ در آرگومان‌های نمادین خط فرمان. برای فعال کردن این گزینه، از -readable-posix-inputs` استفاده کنید. این گزینه به‌طور پیش‌فرض غیرفعال است، زیرا استفاده گسترده از `klee_prefer_cex` می‌تواند پرهزینه باشد.

2.3 آموزش‌ها (Tutorials)

اولین آموزش: آزمایش یک تابع کوچک.

این آموزش شما را از طریق مراحل اصلی لازم برای آزمایش یک تابع ساده با KLEE راهنمایی می‌کند. در اینجا تابع ساده ما آمده است:

				
					int get_sign(int x) {
  if (x == 0)
    return 0;

  if (x &lt; 0)
    return -1;
  else
    return 1;
}

می‌توانید کل کد این مثال را در درخت سورس تحت مسیر `examples/get_sign` پیدا کنید. همچنین نسخه‌ای از کد منبع از اینجا نیز قابل دسترسی است.

2.3.1 علامت‌گذاری یک ورودی به‌عنوان نمادین (Marking input as symbolic):

برای اینکه این تابع را با KLEE آزمایش کنیم، باید آن را روی ورودی نمادین (symbolic input) اجرا کنیم. برای علامت‌گذاری یک متغیر به‌عنوان نمادین، از تابع ()klee_make_symbolic استفاده می‌کنیم (تعریف شده در klee/klee.h) که سه آرگومان می‌گیرد: آدرس متغیر (محل حافظه) که می‌خواهیم به‌صورت نمادین در نظر گرفته شود، اندازه متغیر، یک نام (می‌تواند هر چیزی باشد).

در اینجا یک تابع ساده ()main آمده است که متغیر a را نمادین می‌کند و از آن برای فراخوانی ()get_sign استفاده می‌کند:

				
					int main() {
  int a;
  klee_make_symbolic(&amp;a, sizeof(a), "a");
  return get_sign(a);
}

2.3.2 کامپایل به LLVM bitcode:

KLEE بر روی LLVM bitcode عمل می‌کند. برای اجرای یک برنامه با KLEE، ابتدا باید آن را با استفاده از دستور clang -emit-llvm به LLVM bitcode کامپایل کنید.

از داخل دایرکتوری examples/get_sign:

این کار باید یک فایل get_sign.bc در فرمت LLVM bitcode ایجاد کند. آرگومان I- برای این استفاده می‌شود که کامپایلر بتواند فایل klee/klee.h را پیدا کند، که شامل تعاریف توابع intrinsic مورد استفاده برای تعامل با ماشین مجازی KLEE، مانند klee_make_symbolic است. همچنین مفید است که با g- ساخته شود تا اطلاعات دیباگ به فایل bitcode اضافه شود، که برای تولید آمار سطح خط منبع استفاده می‌کنیم.

فایل bitcode‌ی که به KLEE داده می‌شود نباید بهینه‌سازی شده باشد، زیرا ما به‌صورت دستی بهینه‌سازی‌های مناسب KLEE را انتخاب کرده‌ایم که می‌توانند با گزینه خط فرمان optimize KLEE– فعال شوند. با این حال، در نسخه‌های جدید LLVM (> 5.0)، از فلگ O0- نباید استفاده کرد، زیرا مانع انجام بهینه‌سازی‌های خود KLEE می‌شود. به جای آن باید از -O0 -Xclang -disable-O0-optnone استفاده کنید، برای جزئیات بیشتر این issue را مشاهده کنید.

اگر نمی‌خواهید تست کیس‌ها را طبق توضیح بعدی بازپخش کنید و به اطلاعات دیباگ یا بهینه‌سازی اهمیت نمی‌دهید، می‌توانید include فایل klee/klee.h را حذف کرده و سپس فایل get_sign.c را با دستور زیر کامپایل کنید:

				
					$ clang -emit-llvm -c get_sign.c

با این حال، توصیه می‌کنیم از دستور طولانی‌تر بالا استفاده کنید.

2.3.3 اجرای KLEE:

برای اجرای KLEE روی فایل bitcode کافی است دستور زیر را اجرا کنید:

				
					$ klee get_sign.bc

شما باید خروجی زیر را مشاهده کنید:

				
					KLEE: output directory = "klee-out-0"

KLEE: done: total instructions = 33
KLEE: done: completed paths = 3
KLEE: done: partially completed paths = 0
KLEE: done: generated tests = 3

تابع ساده ما سه مسیر دارد: یکی که `a` برابر ۰ است، یکی که کمتر از ۰ است و یکی که بزرگتر از ۰ است. همان‌طور که انتظار می‌رود، KLEE به ما اطلاع می‌دهد که سه مسیر را در برنامه بررسی کرده و برای هر مسیر یک تست کیس تولید کرده است.

برای برنامه‌های بزرگ‌تر، ممکن است KLEE نتواند هر مسیر را تا انتها بررسی کند به دلیل محدودیت زمان یا حافظه. در این صورت، KLEE همچنین تعداد مسیرهای قطع‌شده (نیمه‌تمام) را گزارش می‌دهد.

خروجی اجرای KLEE یک دایرکتوری است (در مثال ما `klee-out-0`) که شامل تست کیس‌های تولید شده توسط KLEE است. KLEE نام دایرکتوری خروجی را به صورت klee-out-N` می‌گذارد که N کمترین عدد موجود است (بنابراین اگر دوباره KLEE را اجرا کنیم، دایرکتوری‌ای به نام `klee-out-1` ایجاد می‌شود)، و همچنین یک لینک نمادین به نام klee-last` به این دایرکتوری برای راحتی کار ایجاد می‌کند.

				
					$ ls klee-last/
assembly.ll         run.istats       test000002.ktest
info                         run.stats        test000003.ktest
messages.txt     test000001.ktest warnings.txt

لطفاً اینجا کلیک کنید اگر می‌خواهید یک مرور کلی بر فایل‌های تولید شده توسط KLEE داشته باشید. در این آموزش، ما تنها بر فایل‌های واقعی تست تولید شده توسط KLEE تمرکز می‌کنیم.

2.3.4 تست کیس‌های تولید شده توسط KLEE:

تست کیس‌های تولید شده توسط KLEE در فایل‌هایی با پسوند .ktest نوشته می‌شوند. این‌ها فایل‌های باینری هستند که می‌توان با ابزار ktest-tool آن‌ها را خواند.

ktest-tool نمایش‌های مختلفی از یک شیء واحد ارائه می‌دهد، برای مثال: رشته‌های بایت در پایتون (data)، اعداد صحیح (int) یا متن ASCII (text). بنابراین بیایید هر فایل را بررسی کنیم:

در هر فایل تست، KLEE آرگومان‌هایی را که برنامه با آن‌ها فراخوانی شده است گزارش می‌دهد (در مثال ما به جز نام برنامه، آرگومانی وجود ندارد)، تعداد اشیاء نمادین روی آن مسیر (در مثال ما فقط یکی)، نام شیء نمادین ما (`’a’`) و اندازه آن (۴) را نمایش می‌دهد.

خود تست با مقدار ورودی ما نمایش داده می‌شود: ۰ برای اولین تست، ۱۶۸۴۳۰۰۹ برای دومین و -۲۱۴۷۴۸۳۶۴۸ برای آخرین تست. همان‌طور که انتظار می‌رفت، KLEE یک مقدار صفر، یک مقدار مثبت (۱۶۸۴۳۰۰۹) و یک مقدار منفی (-۲۱۴۷۴۸۳۶۴۸) تولید کرده است.

اکنون می‌توانیم این مقادیر را روی نسخه native برنامه خود اجرا کنیم تا تمام مسیرهای کد را پوشش دهیم!

2.3.5 Replay کردن یک تست کیس:

در حالی که می‌توانیم تست کیس‌های تولید شده توسط KLEE را به صورت دستی روی برنامه خود اجرا کنیم (یا با کمک یک زیرساخت تست موجود)، KLEE یک کتابخانه replay راحت ارائه می‌دهد که به سادگی فراخوانی `klee_make_symbolic` را با فراخوانی تابعی جایگزین می‌کند که به ورودی ما مقداری را که در فایل `.ktest` ذخیره شده اختصاص می‌دهد.

برای استفاده از آن، کافی است برنامه خود را با کتابخانه `libkleeRuntest` لینک کنید و متغیر محیطی KTEST_FILE` را به نام تست کیس موردنظر تنظیم کنید:

همان‌طور که انتظار می‌رود، برنامه ما هنگام اجرای اولین تست کیس مقدار ۰، هنگام اجرای دومین تست کیس مقدار ۱ و هنگام اجرای آخرین تست کیس مقدار ۲۵۵ (که -۱ به یک مقدار معتبر خروجی در بازه ۰–۲۵۵ تبدیل شده است) را بازمی‌گرداند.

دومین آموزش: آزمایش یک کتابخانه ساده عبارت‌های منظم (regular expression).

این یک مثال از استفاده KLEE برای آزمایش یک تابع ساده تطبیق عبارت منظم (regular expression) است. می‌توانید مثال پایه را در درخت سورس تحت مسیر examples/regexp پیدا کنید.

فایل Regexp.c شامل یک تابع ساده برای تطبیق عبارت منظم و یک harness تست ابتدایی (در main()) است که برای بررسی این کد با KLEE لازم است. نسخه‌ای از کد منبع نیز از اینجا قابل مشاهده است.

این مثال نشان می‌دهد چگونه می‌توان مثال را با KLEE ساخت و اجرا کرد، نحوه تفسیر خروجی و برخی از ویژگی‌های اضافی KLEE که هنگام نوشتن تست درایور به صورت دستی می‌توان استفاده کرد.

ابتدا نحوه ساخت و اجرای مثال را نشان می‌دهیم و سپس جزئیات بیشتری در مورد نحوه عملکرد harness تست توضیح خواهیم داد.

2.3.6 ایجاد یک نمونه:

اولین مرحله، کامپایل کد منبع با استفاده از یک کامپایلر است که بتواند فایل‌های آبجکت را در فرمت LLVM bitcode تولید کند. از داخل دایرکتوری examples/regexp دستور زیر را اجرا کنید:

این دستور باید یک فایل Regexp.bc در فرمت LLVM bitcode ایجاد کند.

آرگومان I- برای این استفاده می‌شود که کامپایلر بتواند [1]klee/klee.h را پیدا کند، که شامل تعاریف توابع intrinsic مورد استفاده برای تعامل با ماشین مجازی KLEE است.
c- به این دلیل استفاده می‌شود که فقط می‌خواهیم کد را به یک فایل آبجکت کامپایل کنیم (نه به یک اجرایی native).
g- باعث می‌شود اطلاعات دیباگ اضافی در فایل آبجکت ذخیره شود که KLEE از آن برای تعیین شماره خط منبع استفاده می‌کند.
O0 -Xclang -disable-O0-optnone– برای کامپایل بدون بهینه‌سازی، اما بدون جلوگیری از انجام بهینه‌سازی‌های خود KLEE استفاده می‌شود (در حالی که کامپایل با -O0 مانع از انجام بهینه‌سازی‌های KLEE می‌شود).

اگر ابزارهای LLVM در مسیر شما نصب شده باشند، می‌توانید صحت این مرحله را با اجرای llvm-nm روی فایل تولید شده بررسی کنید:

[1] https://github.com/klee/klee/blob/master/include/klee/klee.h

				
					$ llvm-nm Regexp.bc
                 U klee_make_symbolic
---------------- T main
---------------- T match
---------------- t matchhere
---------------- t matchstar

به‌طور معمول، قبل از اجرای این برنامه باید آن را لینک کنیم تا یک فایل اجرایی native ایجاد شود. با این حال، KLEE به‌صورت مستقیم روی فایل‌های LLVM bitcode اجرا می‌شود. از آنجا که این برنامه تنها شامل یک فایل است، نیازی به لینک کردن نیست.

برای برنامه‌های «واقعی» که چندین فایل ورودی دارند، می‌توان از ابزار llvm-link به جای مرحله لینک معمولی استفاده کرد تا چند فایل LLVM bitcode را در یک ماژول واحد ادغام کرد که توسط KLEE قابل اجرا باشد.

2.3.7 اجرای کد توسط KLEE:

گام بعدی اجرای کد توسط KLEE است (تعداد دستورها بسته به نسخه LLVM و سطح بهینه‌سازی متفاوت است):

				
					$ klee --only-output-states-covering-new Regexp.bc
KLEE: output directory = "klee-out-0"
KLEE: ERROR: Regexp.c:23: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: Regexp.c:25: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 4848112
KLEE: done: completed paths = 6675
KLEE: done: partially completed paths = 763
KLEE: done: generated tests = 16

در هنگام شروع، KLEE دایرکتوری‌ای که برای ذخیره خروجی استفاده می‌شود را چاپ می‌کند (در این مثال `klee-out-0`). به‌صورت پیش‌فرض، KLEE از اولین دایرکتوری آزاد `klee-out-N` استفاده می‌کند و همچنین یک لینک نمادین به نام klee-last` ایجاد می‌کند که به آخرین دایرکتوری ایجاد شده اشاره دارد. می‌توانید دایرکتوری موردنظر برای خروجی‌ها را با استفاده از آرگومان خط فرمان -output-dir=path` مشخص کنید.

در حین اجرای KLEE، پیام‌های وضعیت برای رویدادهای «مهم» چاپ می‌شوند، برای مثال زمانی که یک خطا در برنامه پیدا شود. در این مثال، KLEE دو دسترسی غیرمجاز به حافظه در خطوط ۲۳ و ۲۵ برنامه تست ما شناسایی کرده است. کمی بعد به این موضوع دقیق‌تر نگاه خواهیم کرد.

در نهایت، وقتی KLEE اجرای برنامه را به پایان می‌رساند، چند آمار از اجرای برنامه را چاپ می‌کند. در اینجا مشاهده می‌کنیم که KLEE در مجموع حدود ۴.۸ میلیون دستور اجرا کرده، ۷۴۳۸ مسیر را بررسی کرده و ۱۶ تست کیس تولید کرده است. KLEE تنها ۱۶ تست کیس تولید کرده زیرا تولید تست را محدود کرده‌ایم به حالت‌هایی که واقعاً کد جدیدی را پوشش می‌دهند با استفاده از –only-output-states-covering-new`. اگر این فلگ را حذف می‌کردیم، KLEE ۶۶۷۷ تست کیس ایجاد می‌کرد!

با این حال، KLEE برای هر مسیر یک تست کیس ایجاد نمی‌کند. هرگاه یک باگ پیدا شود، KLEE یک تست کیس برای اولین حالت که به باگ می‌رسد ایجاد می‌کند. تمام مسیرهای دیگر که به همان باگ در همان موقعیت برسند، به‌صورت بی‌صدا خاتمه می‌یابند و به‌عنوان مسیرهای نیمه‌تمام گزارش می‌شوند. اگر مشکلی با تکرار حالات خطا ندارید، می‌توانید از –emit-all-errors` استفاده کنید تا برای تمام ۷۴۳۸ مسیر تست کیس تولید شود.

توجه داشته باشید که بسیاری از برنامه‌های واقعی دارای تعداد مسیر بی‌نهایت (یا بسیار زیاد) هستند و معمولاً KLEE خاتمه نمی‌یابد. به‌صورت پیش‌فرض، KLEE تا زمانی اجرا می‌شود که کاربر Control-C فشار دهد (یعنی KLEE یک SIGINT دریافت کند)، اما گزینه‌های اضافی برای محدود کردن زمان اجرا و مصرف حافظه وجود دارد:

-max-time=<time span>: پس از مدت زمان مشخص اجرای برنامه متوقف شود، برای مثال `10min` یا `1h5s`.
-max-forks=N: پس از N شاخه نمادین، فرایند fork متوقف شود و مسیرهای باقی‌مانده تا انتها اجرا شوند.
-max-memory=N: تلاش شود مصرف حافظه به N مگابایت محدود شود.

2.3.8 گزارش خطای KLEE:

هنگامی که KLEE یک خطا در برنامه در حال اجرا تشخیص دهد، یک تست کیس تولید می‌کند که خطا را نمایش می‌دهد و اطلاعات اضافی درباره خطا را در فایلی به نام testN.TYPE.err` می‌نویسد، که در آن `N` شماره تست کیس و `TYPE` نوع خطا را مشخص می‌کند. برخی از انواع خطاهایی که KLEE شناسایی می‌کند عبارت‌اند از:

ptr: ذخیره یا بارگذاری از مکان‌های نامعتبر حافظه.
free: آزادسازی دوباره یا آزادسازی نامعتبر حافظه (`double or invalid free()`).
abort: برنامه تابع `abort()` را فراخوانی کرده است.
assert: یک assertion شکست خورده است.
div: تقسیم یا محاسبه باقیمانده بر صفر شناسایی شده است.
user: مشکلی با ورودی وجود دارد (فراخوانی‌های نامعتبر klee intrinsic) یا نحوه استفاده از KLEE اشتباه است.
exec: مشکلی پیش آمده که مانع اجرای برنامه توسط KLEE شده است؛ برای مثال دستور ناشناخته، فراخوانی یک اشاره‌گر تابع نامعتبر، یا اسمبلی درون خطی.
Model: KLEEقادر به حفظ دقت کامل نبوده و تنها بخشی از حالت برنامه را بررسی می‌کند. به عنوان مثال، اندازه‌های نمادین برای malloc فعلاً پشتیبانی نمی‌شوند و در چنین مواردی KLEE آرگومان را concretize می‌کند.

KLEE هنگام تشخیص خطا یک پیام را در کنسول چاپ می‌کند. در اجرای تست بالا می‌بینیم که KLEE دو خطای حافظه را شناسایی کرده است. برای تمام خطاهای برنامه، KLEE یک backtrace ساده در فایل `.err` می‌نویسد. این نمونه‌ای از یکی از خطاهای فوق است:

				
					Error: memory error: out of bound pointer
File: .../klee/examples/regexp/Regexp.c
Line: 23
Stack:
  #0 00000146 in matchhere (re=14816471, text=14815301) at .../klee/examples/regexp/Regexp.c:23
  #1 00000074 in matchstar (c, re=14816471, text=14815301) at .../klee/examples/regexp/Regexp.c:16
  #2 00000172 in matchhere (re=14816469, text=14815301) at .../klee/examples/regexp/Regexp.c:26
  #3 00000074 in matchstar (c, re=14816469, text=14815301) at .../klee/examples/regexp/Regexp.c:16
  #4 00000172 in matchhere (re=14816467, text=14815301) at .../klee/examples/regexp/Regexp.c:26
  #5 00000074 in matchstar (c, re=14816467, text=14815301) at .../klee/examples/regexp/Regexp.c:16
  #6 00000172 in matchhere (re=14816465, text=14815301) at .../klee/examples/regexp/Regexp.c:26
  #7 00000231 in matchhere (re=14816464, text=14815300) at .../klee/examples/regexp/Regexp.c:30
  #8 00000280 in match (re=14816464, text=14815296) at .../klee/examples/regexp/Regexp.c:38
  #9 00000327 in main () at .../klee/examples/regexp/Regexp.c:59
Info:
  address: 14816471
  next: object at 14816624 of size 4
  prev: object at 14816464 of size 7

هر خط از backtrace شماره فریم، خط دستور (این شماره خط در فایل assembly.ll است که همراه با خروجی اجرا یافت می‌شود)، تابع و آرگومان‌ها (شامل مقادیر پارامترهای concrète) و اطلاعات منبع را لیست می‌کند.

گزارش‌های خطای خاص ممکن است اطلاعات اضافی نیز شامل شوند. برای خطاهای حافظه، KLEE آدرس نامعتبر را نشان می‌دهد و همچنین اشیاء موجود روی heap را قبل و بعد از آن آدرس نمایش می‌دهد. در این مورد، می‌بینیم که آدرس دقیقاً یک بایت بعد از انتهای شیء قبلی قرار دارد.

2.3.9 تغییر هارنس تست (test harness)

دلیل اینکه KLEE خطاهای حافظه در این برنامه پیدا می‌کند، این نیست که توابع عبارت منظم باگ دارند، بلکه نشان‌دهنده مشکل در تست درایور ما است. مشکل این است که ما بافر ورودی عبارت منظم را کاملاً نمادین می‌کنیم، اما تابع match انتظار دارد رشته‌ای با null-terminator باشد. بیایید دو روش برای رفع این مشکل بررسی کنیم.

ساده‌ترین راه برای رفع این مشکل این است که بعد از نمادین کردن بافر، یک ‘\0’ در انتهای آن ذخیره کنیم. در این صورت driver ما به این شکل خواهد بود:

				
					int main() {
  // The input regular expression.
  char re[SIZE];

  // Make the input symbolic.
  klee_make_symbolic(re, sizeof re, "re");
  re[SIZE - 1] = '\0';

  // Try to match against a constant string "hello".
  match(re, "hello");

  return 0;
}

نمادین کردن یک بافر تنها محتویات آن را به متغیرهای نمادین اشاره می‌دهد، و ما همچنان آزاد هستیم حافظه را هر طور که می‌خواهیم تغییر دهیم. اگر این برنامه تست را دوباره کامپایل کرده و KLEE را اجرا کنید، خطاهای حافظه اکنون باید از بین رفته باشند.

روش دیگری برای رسیدن به همان نتیجه استفاده از تابع intrinsic klee_assume است. این تابع یک آرگومان می‌گیرد (یک عدد صحیح بدون علامت) که معمولاً باید یک عبارت شرطی باشد و KLEE فرض می‌کند که این عبارت در مسیر فعلی درست است (اگر این هرگز امکان‌پذیر نباشد، یعنی عبارت به‌صورت اثبات‌شده نادرست باشد، KLEE یک خطا گزارش می‌دهد).

می‌توانیم از klee_assume استفاده کنیم تا KLEE تنها حالت‌هایی را بررسی کند که رشته با null خاتمه یافته است، با نوشتن driver به این شکل:

				
					int main() {
  // The input regular expression.
  char re[SIZE];

  // Make the input symbolic.
  klee_make_symbolic(re, sizeof re, "re");
  klee_assume(re[SIZE - 1] == '\0');

  // Try to match against a constant string "hello".
  match(re, "hello");
  return 0;
}

در این مثال خاص، هر دو راه‌حل به‌خوبی کار می‌کنند، اما به‌طور کلی klee_assume“ انعطاف‌پذیری بیشتری دارد:

با اعلام صریح قید، این روش باعث می‌شود که تست کیس‌ها حتماً شامل `’\0’` باشند. در مثال اول که null خاتمه‌دهنده را به‌صورت صریح می‌نویسیم، مهم نیست که آخرین بایت ورودی نمادین چه مقداری دارد و KLEE آزاد است هر مقداری تولید کند. در برخی موارد که می‌خواهید تست کیس‌ها را به‌صورت دستی بررسی کنید، این راحت‌تر است که تست کیس تمام مقادیری که اهمیت دارند را نشان دهد.

`klee_assume` می‌تواند برای رمزگذاری قیدهای پیچیده‌تر استفاده شود. برای مثال، می‌توانیم از دستور `klee_assume(re[0] != ‘^’)` استفاده کنیم تا KLEE تنها حالت‌هایی را بررسی کند که اولین بایت برابر با ‘^’ نباشد.

توجه: یک نکته مهم هنگام استفاده از `klee_assume` با چند شرط وجود دارد. به خاطر داشته باشید که شرط‌های بولی مانند `&&` و `||` ممکن است به کدی کامپایل شوند که قبل از محاسبه نتیجه عبارت، شاخه‌زنی انجام دهد. در چنین شرایطی، KLEE قبل از رسیدن به فراخوانی `klee_assume` شاخه‌زنی می‌کند، که ممکن است منجر به بررسی حالت‌های اضافی غیرضروری شود. به همین دلیل، بهتر است از عبارات ساده‌تر برای `klee_assume` استفاده شود (مثلاً تقسیم یک فراخوانی به چند فراخوانی) و از عملگرهای `&` و `|` به جای کوتاه‌مدت‌ها (short-circuiting) استفاده کنید.

استفاده از محیط نمادین (symbolic environment): راهنمایی همراه با مثال برای استفاده از محیط نمادین، شامل فایل‌های نمادین و آرگومان‌های خط فرمان برای برنامه مورد آزمایش.

همان‌طور که در مرور گزینه‌های خط فرمان پایه KLEE ذکر شد، KLEE چندین گزینه به‌عنوان بخشی از محیط نمادین خود ارائه می‌دهد. با این حال، استفاده از آن‌ها برای کاربران جدید اغلب به‌راحتی قابل درک نیست. این آموزش نمونه‌های پایه‌ای از استفاده از -sym-arg` و -sym-files` را ارائه می‌دهد، که شاید مهم‌ترین گزینه‌ها باشند.

sym-arg Usage-

توجه داریم که -sym-arg <N>` یک آرگومان خط فرمان با طول N به برنامه تحت تست ارائه می‌دهد. نسخه دیگر آن، -sym-args <MIN> <MAX> <N>` حداقل MIN و حداکثر MAX آرگومان نمادین را ایجاد می‌کند، که هر کدام حداکثر طول N دارند.

برای نشان دادن استفاده از `-sym-arg`، ابتدا برنامه زیر password.c` را در نظر می‌گیریم که آرگومان خط فرمان را برای مطابقت با یک پسورد hard-coded بررسی می‌کند.

				
					#include 

int check_password(char *buf) {
  if (buf[0] == 'h' &amp;&amp; buf[1] == 'e' &amp;&amp;
      buf[2] == 'l' &amp;&amp; buf[3] == 'l' &amp;&amp;
      buf[4] == 'o')
    return 1;
  return 0;
}

int main(int argc, char argv) {
  if (argc &lt; 2)
     return 1;
  
  if (check_password(argv[1])) {
    printf(&quot;Password found!\n&quot;);
    return 0;
  }

  return 1;
}

برای فعال کردن محیط نمادین، باید به KLEE گزینه -posix-runtime داده شود. برنامه KLEE را با bitcode فایل password.c به‌عنوان ورودی و با استفاده از گزینه -sym-arg به‌صورت زیر اجرا می‌کنیم:

				
					$ clang -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone password.c
$ klee -posix-runtime password.bc -sym-arg 5
KLEE: NOTE: Using model: /home/klee/klee/build/Release+Debug+Asserts/lib/libkleeRuntimePOSIX64_Release+Debug+Asserts.bca
KLEE: output directory is "/home/klee/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING: undefined reference to function: printf
KLEE: WARNING: undefined reference to function: strlen
KLEE: WARNING: undefined reference to function: strncmp
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: calling external: syscall(4, 94328563719264, 94328559327712) at /home/klee/klee/runtime/POSIX/fd.c:544 12
KLEE: WARNING ONCE: calling __klee_posix_wrapped_main with extra arguments.
KLEE: WARNING ONCE: calling external: printf(94328563829504) at password.c:17 5
Password found!

KLEE: done: total instructions = 1190
KLEE: done: completed paths = 6
KLEE: done: partially completed paths = 0
KLEE: done: generated tests = 6

همان‌طور که مشاهده می‌شود، به دلیل اینکه آرگومان خط فرمان نمادین بود، KLEE شش مسیر را اجرا کرد، که در یکی از مسیرها آرگومان خط فرمان با پسورد مطابقت داشت.

sym-files Usage-

گزینه -sym-files <NUM> <N> تعداد NUM فایل نمادین ایجاد می‌کند، که اولین فایل با نام «A»، دومین با نام «B» و به همین ترتیب نام‌گذاری می‌شوند، و هر فایل اندازه N دارد. گزینه‌های مشابه آن، -sym-stdin و -sym-stdout به ترتیب ورودی و خروجی استاندارد را نمادین می‌کنند.

حال یک چکر پسورد را در نظر می‌گیریم، همچنان با نام password.c، که یک رشته را از فایلی که کاربر مشخص می‌کند می‌خواند و بررسی می‌کند که آیا با پسورد hard-coded مطابقت دارد یا خیر. اگر نام فایل مشخص نشده باشد، یا هنگام باز کردن فایل خطایی رخ دهد، رشته را از ورودی استاندارد می‌خواند.

				
					#include 
#include 
#include 
#include 
#include 

int check_password(int fd) {
  char buf[5];
  if (read(fd, buf, 5) != -1) {
    if (buf[0] == 'h' &amp;&amp; buf[1] == 'e' &amp;&amp;
	buf[2] == 'l' &amp;&amp; buf[3] == 'l' &amp;&amp;
	buf[4] == 'o')
      return 1;
  }
  return 0;
}

int main(int argc, char argv) {
  int fd;

  if (argc &gt;= 2) {
    if ((fd = open(argv[1], O_RDONLY)) != -1) {
      if (check_password(fd)) {
        printf("Password found in %s\n", argv[1]);
        close(fd);
        return 0;
      }
      close(fd);
      return 1;
    }
  }
  if (check_password(0)) {
    printf("Password found in standard input\n");
    return 0;
  }
  return 1;
}

حال برنامه را با استفاده از KLEE اجرا می‌کنیم. برای اینکه برنامه هنگام خواندن داده گیر نکند، باید مقداری ورودی فراهم کنیم. در اولین اجرای ما، یک ورودی استاندارد نمادین با استفاده از گزینه sym-stdin- ارائه می‌کنیم. این ورودی نمادین باعث می‌شود که KLEE مسیر بررسی موفقیت‌آمیز پسورد را نیز بررسی کند.

				
					$ clang -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone password.c
$ klee -posix-runtime password.bc -sym-stdin 10
KLEE: NOTE: Using model: /home/klee/klee/build/Release+Debug+Asserts/lib/libkleeRuntimePOSIX64_Release+Debug+Asserts.bca
KLEE: output directory is "/home/klee/klee-out-1"
KLEE: Using STP solver backend
KLEE: WARNING: undefined reference to function: printf
KLEE: WARNING: undefined reference to function: strlen
KLEE: WARNING: undefined reference to function: strncmp
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: calling external: syscall(4, 94571123861232, 94571119847248) at /home/klee/klee/runtime/POSIX/fd.c:544 12
KLEE: WARNING ONCE: calling __klee_posix_wrapped_main with extra arguments.
KLEE: WARNING ONCE: calling external: printf(94571123946704) at password.c:35 5
Password found in standard input

KLEE: done: total instructions = 1856
KLEE: done: completed paths = 6
KLEE: done: partially completed paths = 0
KLEE: done: generated tests = 6

اکنون با استفاده از KLEE پسورد را کشف کرده‌ایم.

برنامه ما همچنین می‌تواند پسورد را از یک فایل روی دیسک بخواند، اما می‌خواهیم یک فایل با محتوای نمادین بخوانیم تا KLEE مسیر موفقیت‌آمیز بودن بررسی پسورد را اجرا کند. گزینه -sym-files چندین فایل این ‌چنینی با نام‌های «A»، «B»، «C» و غیره فراهم می‌کند. با مشخص کردن گزینه -sym-files 1 10 در این مثال، از KLEE می‌خواهیم یک فایل نمادین به اندازه ۱۰ بایت ارائه دهد، که این فایل توسط KLEE با نام «A» نام‌گذاری می‌شود. بنابراین، ما این نام فایل را به‌عنوان آرگومان به برنامه می‌دهیم.

				
					$ klee -posix-runtime password.bc A -sym-files 1 10
KLEE: NOTE: Using model: /home/klee/klee/build/Release+Debug+Asserts/lib/libkleeRuntimePOSIX64_Release+Debug+Asserts.bca
KLEE: output directory is "/home/klee/klee-out-2"
KLEE: Using STP solver backend
KLEE: WARNING: undefined reference to function: printf
KLEE: WARNING: undefined reference to function: strlen
KLEE: WARNING: undefined reference to function: strncmp
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: calling external: syscall(4, 94110989166360, 94110985152336) at /home/klee/klee/runtime/POSIX/fd.c:544 12
KLEE: WARNING ONCE: calling __klee_posix_wrapped_main with extra arguments.
KLEE: WARNING ONCE: calling external: printf(94110989239968, 94110989166176) at password.c:25 15
Password found in A

KLEE: done: total instructions = 4395
KLEE: done: completed paths = 6
KLEE: done: partially completed paths = 0
KLEE: done: generated tests = 6

پسورد در یکی از مسیرهای اجرا با موفقیت از فایل نمادین «A» خوانده شد.

آزمایش Coreutils: توضیح مفصل درباره نحوه استفاده از KLEE برای آزمایش [1]GNU Coreutils.

به عنوان شرح جزئيات بيشتر از به کارگيري KLEE، نگاهي مي اندازيم به نحوه سنجش GNU Coreutils با KLEE. لطفا دستورهاي توضيح داده شده در آزمايش coreutils مقاله OSDI’08 ما را دنبال کنيد تا تنظيمات آزمايش مقاله را بازتوليد کنيد. اين آموزش فرض مي کند که شما KLEE را با پشتيباني uclibc و محيط اجراي POSIX پيكربندي و ساخته ايد. تمامي آزمون ها روي يک سامانه ۶۴ بيتي لينوکسي انجام شده اند.

گام ۱: ساخت coreutils با پشتيباني gcov

ابتدا بايد سورس [4]coreutils را دريافت و از حالت فشرده بيرون بياوريد. در اين نمونه ما نگارش 6.11 را به کار مي بريم (يک نگارش پس از آنچه در مقاله OSDI خود استفاده کرديم) اما مي توانيد هر نگارش ديگري از Coreutils را به کار ببريد. توجه کنيد که نگارش هاي کهنه براي کار کردن روي سامانه هاي تازه نياز به اصلاح دارند. جزئيات و دستورهاي آن در اينجا قابل دسترس است. همچنين براي نگارش هاي تازه، گام make -C src arch hostname را مي توان کنار گذاشت.

پيش از آنکه با LLVM بسازيم، بياييد يک نگارش از coreutils را با پشتيباني gcov بسازيم. بعدا از اين براي به دست آوردن اطلاعات پوشش (coverage) بر روي نمونه هاي سنجش که KLEE توليد مي کند استفاده خواهيم کرد.

درون پوشه coreutils، گام هاي هميشگي configure و make را در يک زيرپوشه (obj-gcov) انجام مي دهيم. اين گام ها به شرح زير هستند:

				
					coreutils-6.11$ mkdir obj-gcov
coreutils-6.11$ cd obj-gcov
obj-gcov$ ../configure --disable-nls CFLAGS="-g -fprofile-arcs -ftest-coverage"
... verify that configure worked ...
obj-gcov$ make
obj-gcov$ make -C src arch hostname
... verify that make worked ...

ما با گزينه ‑‑disable-nls مي سازيم چون اين گزينه مقدار زيادي آماده سازي آغازين در کتابخانه C اضافه مي کند که نمي خواهيم آن را سنجش کنيم. هرچند اينها اجراشدني هايي نيستند که KLEE آن ها را به کار خواهد انداخت، اما مي خواهيم همان پرچم هاي کامپايلر (compiler flags) را به کار ببريم تا نمونه هاي سنجش که KLEE توليد مي کند بيشترين احتمال را داشته باشند که هنگام اجرا روي باینری هاي بدون ابزارکاري (uninstrumented binaries) درست عمل کنند.

اکنون بايد يک مجموعه از coreutils در پوشه objc-gcov/src داشته باشيد. براي نمونه:

				
					obj-gcov$ cd src
src$ ls -l ls echo cat
-rwxrwxr-x 1 klee klee 150632 Nov 21 21:58 cat
-rwxrwxr-x 1 klee klee 135984 Nov 21 21:58 echo
-rwxrwxr-x 1 klee klee 390552 Nov 21 21:58 ls
src$ ./cat --version
cat (GNU coreutils) 6.11
Copyright (C) 2008 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.

Written by Torbjorn Granlund and Richard M. Stallman.

علاوه بر اين، اين اجراشدني ها بايد با پشتيباني gcov ساخته شوند، به طوري که اگر يکي از آن ها را اجرا کنيد، يک فايل gcda. در پوشه جاري نوشته مي شود. اين فايل شامل اطلاعات دقيق درباره اين است که هنگام اجراي برنامه کدام بخش هاي کد اجرا شده اند. براي اطلاعات بيشتر به مستندات Gcov مراجعه کنيد. ما مي توانيم از ابزار gcov خود براي توليد فرم قابل خواندن انسان از داده هاي پوشش استفاده کنيم. براي نمونه:

به طور پيش فرض، gcov تعداد خطوط اجرا شده در برنامه را نشان مي دهد (فايل هاي h. شامل کدي هستند که در echo.c کامپايل شده اند).

گام ۲: نصب WLLVM

يکي از بخش هاي دشوار در سنجش نرم افزار واقعي با KLEE اين است که ابتدا بايد برنامه به گونه اي کامپايل شود که برنامه نهايي يک فايل بيت‌کد LLVM باشد و نه يک باینری بومي. سامانه ساخت نرم افزار ممکن است براي استفاده از ابزارهايي مانند ‘ar’، ‘libtool’ و ‘ld’ تنظيم شده باشد، که عموما فايل هاي بيت‌کد LLVM را نمي شناسند.

براي coreutils، ما از whole-program-llvm (WLLVM) استفاده مي کنيم، که ابزارهايي براي ساخت فايل هاي بيت‌کد LLVM تمام برنامه از بسته سورس C يا ++C بدون تغيير فراهم مي کند. WLLVM شامل چهار اجرايي پایتوني است: wllvm يک کامپايلر C و wllvm++ يک کامپايلر ++C، ابزار extract-bc براي استخراج بيت‌کد از محصول ساخت (چه فايل شي، اجراشدني، کتابخانه يا آرشيو)، و ابزار wllvm-sanity-checker براي تشخيص نقص هاي پيكربندي. در اين آموزش، ما از نگارش 1.0.17 WLLVM استفاده مي کنيم.

راحت ترين روش براي نصب whole-program-llvm استفاده از pip است:

				
					$ pip install --upgrade wllvm

براي اجراي موفق WLLVM لازم است متغير محيطي LLVM_COMPILER را به کامپايلر LLVM پايه (يا dragonegg يا clang) تنظيم کنيم. در اين آموزش، ما از clang استفاده مي کنيم:

				
					$ export LLVM_COMPILER=clang

ما مانند قبل، يک پوشه جداگانه مي سازيم تا بتوانيم به سادگي هم به اجراشدني هاي بومي و هم به نگارش هاي LLVM دسترسي داشته باشيم. گام ها به شرح زير می‌باشند:

				
					coreutils-6.11$ mkdir obj-llvm
coreutils-6.11$ cd obj-llvm
obj-llvm$ CC=wllvm ../configure --disable-nls CFLAGS="-g -O1 -Xclang -disable-llvm-passes -D__NO_STRING_INLINES  -D_FORTIFY_SOURCE=0 -U__OPTIMIZE__"
... verify that configure worked ...
obj-llvm$ make
obj-llvm$ make -C src arch hostname
... verify that make worked ...

توجه کنيد که ما دو تغيير اعمال کرديم. اول، نمي خواهيم ابزارکاري gcov را در باینری که قرار است با KLEE سنجش شود اضافه کنيم، بنابراين فلگ هاي -fprofile-arcs و -ftest-coverage را حذف کرديم. دوم، فلگ هاي -O1 و -Xclang -disable-llvm-passes را به CFLAGS افزوديم. اين مشابه افزودن -O0 است، اما در LLVM نگارش 5.0 و بالاتر، کامپايل با -O0 مانع از آن مي شود که KLEE بهينه سازي هاي خود را انجام دهد (که بعدا انجام خواهيم داد). بنابراين، ما با -O1 کامپايل مي کنيم اما همه بهينه سازي ها را به طور صريح غیرفعال مي کنيم. براي جزئيات بيشتر به اين مسئله مراجعه کنيد.

توجه داشته باشيد که مي توانستيم از -O0 -Xclang -disable-O0-optnone نيز استفاده کنيم، اما چون قرار است بعدا Coreutils را با بهينه سازي اجرا کنيم، بهتر است با -O1 -Xclang -disable-llvm-passes کامپايل شود. نگارش -O1 بيت‌کدي توليد مي کند که براي بهينه سازي مناسب تر است، بنابراين در اين مورد ترجيح داده مي شود از آن استفاده شود.

-D__NO_STRING_INLINES -D_FORTIFY_SOURCE=0 -U__OPTIMIZE__ يک مجموعه ديگر از فلگ هاي مهم است. در نگارش هاي بعدي LLVM، clang نسخه امن برخي توابع کتابخانه اي را توليد مي کند. براي نمونه، fprintf را با __fprintf_chk جايگزين مي کند که KLEE آن را مدل سازي نمي کند. اين بدان معناست که آن را به عنوان يک تابع خارجي در نظر گرفته و حالت را مشخص مي کند که به نتايج غيرمنتظره منجر خواهد شد.

اگر همه چيز درست پيش رفته باشد، اکنون بايد باینری هاي Coreutils را داشته باشيد. براي نمونه:

				
					obj-llvm$ cd src
src$ ls -l ls echo cat
-rwxrwxr-x 1 klee klee 105448 Nov 21 12:03 cat
-rwxrwxr-x 1 klee klee  95424 Nov 21 12:03 echo
-rwxrwxr-x 1 klee klee 289624 Nov 21 12:03 ls
src$ ./cat --version
cat (GNU coreutils) 6.11
Copyright (C) 2008 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.

Written by Torbjorn Granlund and Richard M. Stallman.

ممکن است متوجه شويد که به جاي فايل هاي بيت‌کد LLVM، باینری هاي اجراشدني به دست آمده اند. اين به اين دليل است که WLLVM در دو مرحله کار مي کند. در مرحله اول، WLLVM کامپايلر استاندارد را فرا مي خواند و سپس براي هر فايل شئ، کامپايلر بيت‌کد را نيز فرا مي خواند تا بيت‌کد LLVM توليد شود. WLLVM مکان فايل هاي بيت‌کد توليد شده را در بخشي اختصاصي از فايل شئ ذخيره مي کند. هنگام پيوند دادن فايل هاي شئ با يکديگر، مکان ها به هم متصل مي شوند تا مکان تمام فايل هاي تشکيل دهنده ذخيره شود. پس از اتمام ساخت، مي توان از ابزار extract-bc WLLVM براي خواندن محتواي بخش اختصاصي و پيوند همه بيت‌کدها به يک فايل بيت‌کد تمام برنامه استفاده کرد.

براي به دست آوردن نگارش بيت‌کد LLVM از تمام Coreutils، مي توان extract-bc را روي تمام باینری هاي اجراشدني فراخواند:

				
					src$ find . -executable -type f | xargs -I '{}' extract-bc '{}'
src$ ls -l ls.bc
-rw-rw-r-- 1 klee klee 543052 Nov 21 12:03 ls.bc

گام ۴: استفاده از KLEE به عنوان مفسر

در اصل، KLEE فقط يک مفسر براي بيت‌کد LLVM است. براي نمونه، در اينجا نحوه اجراي همان دستور cat که پيشتر انجام داديم با استفاده از KLEE آمده است. توجه داشته باشيد، اين گام نياز دارد که KLEE را با پشتيباني uclibc و محيط اجراي POSIX پيكربندي و ساخته باشيد (اگر اين کار را نکرده ايد، اکنون بايد اين کار را انجام دهيد).

				
					src$ klee --libc=uclibc --posix-runtime ./cat.bc --version
KLEE: NOTE: Using klee-uclibc : /usr/local/lib/klee/runtime/klee-uclibc.bca
KLEE: NOTE: Using model: /usr/local/lib/klee/runtime/libkleeRuntimePOSIX.bca
KLEE: output directory is "/home/klee/coreutils-6.11/obj-llvm/src/./klee-out-0"
Using STP solver backend
KLEE: WARNING ONCE: function "vasnprintf" has inline asm
KLEE: WARNING: undefined reference to function: __ctype_b_loc
KLEE: WARNING: undefined reference to function: klee_posix_prefer_cex
KLEE: WARNING: executable has module level assembly (ignoring)
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 42637408)
KLEE: WARNING ONCE: calling __user_main with extra arguments.
KLEE: WARNING ONCE: calling external: getpagesize()
KLEE: WARNING ONCE: calling external: vprintf(43649760, 51466656)
cat (GNU coreutils) 6.11

License GPLv3+: GNU GPL version 3 or later
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.

Written by Torbjorn Granlund and Richard M. Stallman.
Copyright (C) 2008 Free Software Foundation, Inc.
KLEE: WARNING ONCE: calling close_stdout with extra arguments.

KLEE: done: total instructions = 28988
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1

ما اين بار خروجي بسيار بيشتري دريافت کرديم! بياييد گام به گام آن را بررسي کنيم، ابتدا با خود فرمان KLEE. فرم عمومي يک خط فرمان KLEE ابتدا آرگومان هاي خود KLEE، سپس فايل بيت‌کد LLVM براي اجرا (cat.bc) و در نهايت هر آرگوماني که بايد به برنامه منتقل شود (در اين نمونه –version، همانند قبل) است.

اگر يک برنامه بومی عادي اجرا مي شد، با کتابخانه C پيوند مي خورد، اما در اين حالت KLEE مستقيما فايل بيت‌کد LLVM را اجرا مي کند. براي آنکه KLEE به طور مؤثر کار کند، نياز دارد که تعاريف تمام توابع خارجي که برنامه ممکن است فراخواني کند را داشته باشد. ما پياده سازي کتابخانهC به نام uClibc را براي استفاده با KLEE تعديل کرده ايم؛ آرگومان –libc=uclibc به KLEE مي گويد که آن کتابخانه را بارگذاري کرده و قبل از آغاز اجرا با برنامه پيوند دهد.

به همين ترتيب، يک برنامه بومی روي يک سامانه عامل اجرا مي شود که امکانات پايين تر مانند ()write را فراهم مي کند، که کتابخانه C در پياده سازي خود از آن استفاده مي‌کند. همانند قبل، KLEE براي درک کامل برنامه نياز به تعاريف اين توابع دارد. ما يک محيط اجراي POSIX ارائه مي دهيم که براي کار با KLEE و کتابخانه uClibc طراحي شده و بخش عمده امکانات سامانه عامل مورد استفاده برنامه هاي خط فرمان را فراهم مي کند – آرگومان –posix-runtime به KLEE مي گويد که اين کتابخانه را نيز پيوند دهد.

همانند قبل، cat اطلاعات نسخه خود را چاپ مي کند (توجه کنيد که اين بار تمام متن نوشته شده است)، اما اکنون تعداد زيادي اطلاعات اضافي توسط KLEE چاپ مي شود. در اين مورد، بيشتر اين هشدارها بي ضرر هستند، اما براي کمال، معاني آن ها به شرح زير است:

undefined reference to function: ___ctype_b_loc: اين هشدار به اين معناست که برنامه فراخواني تابع __ctype_b_loc را دارد، اما آن تابع در هيچ جايي تعريف نشده است (اگر با uClibc و محيط POSIX پيوند نمي شديم، تعداد زيادي از اين هشدارها ديده مي شد). اگر برنامه در حين اجرا واقعا اين تابع را فراخواني کند، KLEE قادر به تفسير آن نخواهد بود و ممکن است برنامه را خاتمه دهد.

executable has module level assembly (ignoring): بعضي فايل ها که در برنامه کامپايل شده اند شامل اسمبلی در سطح فايل هستند که KLEE قادر به درک آن نيست. در اين مورد، اين از uClibc مي آيد و استفاده نشده است، بنابراين بي خطر است.

calling __user_main with extra arguments: اين نشان مي دهد که تابع با آرگومان هاي بيش از حد انتظار فراخواني شده است، که تقريباً هميشه بي خطر است. در اين مورد user_mainـــ در واقع تابع ()main براي cat است، که KLEE هنگام پيوند با uClibc آن را بازنامگذاري کرده است. ()main توسط خود uClibc در هنگام آغاز با آرگومان هاي اضافي فراخواني مي شود، مانند اشاره گر محيط (environment pointer).

()calling external: getpagesize: اين نمونه اي از فراخواني تابعي است که در برنامه استفاده شده اما هرگز تعريف نشده است. در چنين مواردي، KLEE تلاش مي کند نسخه بومی آن تابع را فراخواني کند، اگر موجود باشد. اين گاهي بي خطر است، تا زماني که آن تابع حافظه برنامه را دستکاری نکند يا سعي در تغيير مقادير نمادين نداشته باشد. براي نمونه، getpagesize() تنها يک مقدار ثابت بازمي گرداند.

به طور کلي، KLEE فقط يک هشدار معین را يک بار چاپ مي کند. اين هشدارها نيز در فايل warnings.txt در پوشه خروجي KLEE ثبت مي شوند.

گام ۵: وارد کردن داده هاي نمادين به برنامه

ديديم که KLEE مي تواند يک برنامه را به طور عادي تفسير کند، اما هدف واقعي KLEE بررسي جامع تر برنامه ها با نمادين کردن بخش هايي از ورودي آن ها است. براي نمونه، بياييد اجراي KLEE روي برنامه echo را بررسي کنيم.

هنگام استفاده از uClibc و محيط اجراي POSIX، KLEE تابع main() برنامه را با يک تابع خاص (klee_init_env) که داخل کتابخانه محيط اجرا ارائه شده است جايگزين مي کند. اين تابع پردازش معمول خط فرمان برنامه را تغيير مي دهد، به ويژه براي پشتيباني از ساخت آرگومان هاي نمادين. براي نمونه، با عبور آرگومان –help نتيجه زير حاصل مي شود:

				
					src$ klee --libc=uclibc --posix-runtime ./echo.bc --help
...

usage: (klee_init_env) [options] [program arguments]
  -sym-arg               - Replace by a symbolic argument with length N
  -sym-args    - Replace by at least MIN arguments and at most
                              MAX arguments, each with maximum length N
  -sym-files        - Make NUM symbolic files ('A', 'B', 'C', etc.),
                              each with size N
  -sym-stdin             - Make stdin symbolic with size N.
  -sym-stdout               - Make stdout symbolic.
  -max-fail              - Allow up to N injected failures
  -fd-fail                  - Shortcut for '-max-fail 1'
...

به عنوان مثال، بیایید دستور echo را با یک آرگومان نمادین ۳ کاراکتری اجرا کنیم.

				
					src$ klee --libc=uclibc --posix-runtime ./echo.bc --sym-arg 3
KLEE: NOTE: Using klee-uclibc : /usr/local/lib/klee/runtime/klee-uclibc.bca
KLEE: NOTE: Using model: /usr/local/lib/klee/runtime/libkleeRuntimePOSIX.bca
KLEE: output directory is "/home/klee/coreutils-6.11/obj-llvm/src/./klee-out-1"
Using STP solver backend
KLEE: WARNING ONCE: function "vasnprintf" has inline asm
KLEE: WARNING: undefined reference to function: __ctype_b_loc
KLEE: WARNING: undefined reference to function: klee_posix_prefer_cex
KLEE: WARNING: executable has module level assembly (ignoring)
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 39407520)
KLEE: WARNING ONCE: calling __user_main with extra arguments.
..
KLEE: WARNING: calling close_stdout with extra arguments.
...
KLEE: WARNING ONCE: calling external: printf(42797984, 41639952)
..
KLEE: WARNING ONCE: calling external: vprintf(41640400, 52740448)
..
Echo the STRING(s) to standard output.

  -n             do not output the trailing newline
  -e             enable interpretation of backslash escapes
  -E             disable interpretation of backslash escapes (default)
      --help     display this help and exit
      --version  output version information and exit
Usage: ./echo.bc [OPTION]... [STRING]...
echo (GNU coreutils) 6.11
Copyright (C) 2008 Free Software Foundation, Inc.
If -e is in effect, the following sequences are recognized:

  \0NNN   the character whose ASCII code is NNN (octal)
  \\     backslash
  \a     alert (BEL)
  \b     backspace

License GPLv3+: GNU GPL version 3 or later
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.

  \c     suppress trailing newline
  \f     form feed
  \n     new line
  \r     carriage return
  \t     horizontal tab
  \v     vertical tab

NOTE: your shell may have its own version of echo, which usually supersedes
the version described here.  Please refer to your shell's documentation
for details about the options it supports.

Report bugs to .
Written by FIXME unknown.

KLEE: done: total instructions = 64546
KLEE: done: completed paths = 25
KLEE: done: generated tests = 25

نتايج اينجا کمي جالب تر هستند، KLEE بيست و پنج مسير را از درون برنامه بررسي کرده است. خروجي همه اين مسيرها در هم آميخته است، اما ميتوان ديد که افزون بر تکرار کاراکترهاي تصادفي گوناگون، برخي بلوک هاي متن نيز چاپ شده اند. شايد برايتان شگفت آور باشد که echo در coreutils چند آرگومان ميگيرد؛ در اين مورد، گزينه هاي v دو خط تيره کوتاه شده version دو خط تيره و h دو خط تيره کوتاه شده help دو خط تيره بررسي شده اند. ميتوانيم يک خلاصه کوتاه از آمارهاي دروني KLEE را با اجراي klee stats بر روي پوشه خروجي به دست آوريم، به ياد داشته باشيد که KLEE هميشه يک symlink به نام klee last براي جديدترين پوشه خروجي ايجاد ميکند.

				
					src$ klee-stats klee-last
------------------------------------------------------------------------
|  Path   |  Instrs|  Time(s)|  ICov(%)|  BCov(%)|  ICount|  TSolver(%)|
------------------------------------------------------------------------
|klee-last|   64546|     0.15|    22.07|    14.14|   19943|       62.97|
------------------------------------------------------------------------

‌اينجا ICov درصد دستورهاي LLVM است که پوشش داده شده‌اند، و BCov درصد شاخه هايي است که پوشش داده شدهاند. شايد بپرسيد چرا درصدها اين قدر پايين هستند؛ مگر echo چقدر کدِ بيشتر ميتواند داشته باشد! دليل اصلي اين است که اين اعداد با استفاده از همه دستورها يا شاخه‌هاي موجود در فايل‌هاي bitcode محاسبه مي‌شوند؛ اين شامل مقدار زيادي کد کتابخانه‌اي است که شايد حتي قابل اجرا هم نباشد. ميتوانيم با دادن گزينه optimize دو خط تيره به KLEE در حل اين مشکل و برخي مشکلات ديگر کمک کنيم. اين کار باعث مي‌شود KLEE گذرهاي بهينه سازي LLVM را پيش از اجرا بر روي ماژول bitcode اعمال کند؛ به ويژه اين گذرها هر کد مرده‌اي را حذف خواهند کرد. هنگام کار با برنامه هاي غير ساده، تقريبا هميشه ايده خوبي است که از اين پرچم استفاده کنيد. در اينجا نتايج حاصل از اجراي دوباره با فعال بودن optimize دو خط تيره آمده است.

				
					src$ klee --optimize --libc=uclibc --posix-runtime ./echo.bc --sym-arg 3
...
KLEE: done: total instructions = 33991
KLEE: done: completed paths = 25
KLEE: done: generated tests = 25
src$ klee-stats klee-last
------------------------------------------------------------------------
|  Path   |  Instrs|  Time(s)|  ICov(%)|  BCov(%)|  ICount|  TSolver(%)|
------------------------------------------------------------------------
|klee-last|   33991|     0.13|    30.16|    21.91|    8339|       80.66|
------------------------------------------------------------------------

اين بار پوشش دستورها حدود شش درصد افزايش پيدا کرد، و ميبينيد که KLEE همچنين سريع تر اجرا شد و دستورهاي کمتري را اجرا کرد. بيشتر کد باقي مانده هنوز در توابع کتابخانه اي است، فقط در بخش هايي که بهينه سازها به اندازه کافي هوشمند نيستند که آنها را حذف کنند. ميتوانيم اين را راستی آزمایی کنيم و براي يافتن کد پوشش نيافته درون echo از KCachegrind براي ديدارسازي نتايج يک اجراي KLEE استفاده کنيم.

گام شش: ديدارسازي پيشرفت KLEE با kcachegrind

KCachegrind يک ابزار بسيار عالی برای ديدارسازی پروفايل‌گيری (profiling) است که در اصل برای استفاده همراه با افزونه کال‌گرایند (callgrind) در وال‌گرایند (valgrind) نوشته شده بود. اگر آن را از پيش نصب نکرده‌اید، معمولا در توزيع‌های مدرن لينوکس از طريق ابزار مديريت نرم‌افزار سيستم‌تان مانند apt-get يا yum به‌سادگی در دسترس است.

KLEE به طور پيش‌فرض يک فايل run.istats در پوشه خروجی آزمون می‌نويسد که در واقع يک فايل کی‌کَش‌گرایند (KCachegrind) است. در اين مثال، run.istats از يک اجرا بدون گزينه optimize دو خط تيره (optimize–) است، بنابراين نتايج فهم‌پذيرتر هستند. اگر KCachegrind را نصب کرده‌ايد، کافی است اجرا کنيد:

				
					src$ kcachegrind klee-last/run.istats

پس از باز شدن KCachegrind بايد پنجره‌ای ببينيد که شبيه تصوير زير است. بايد مطمئن شويد که آمار Instructions (دستورها) انتخاب شده است؛ برای اين کار از منوی View سپس Primary Event Type سپس Instructions آن را انتخاب کنید. همچنين مطمئن شويد که نمايش کد منبع (Source Code) انتخاب شده است؛ اين همان پنجره سمت راست در تصوير زير است.

KCachegrind خودش يک برنامه پيچيده است و کاربران علاقمند بايد برای اطلاعات و مستندات بيشتر به وب‌سايت KCachegrind مراجعه کنند. با اين حال، نکته‌های پايه اين است که يکی از پنجره‌ها «نمايه تخت» (Flat Profile) را نشان می‌دهد؛ اين فهرستی است از اين‌که در هر تابع چه تعداد دستور (instructions) اجرا شده است. ستون Self تعداد دستورهايی است که در خودِ تابع اجرا شده‌اند، و ستون Incl فراگير (inclusive) تعداد دستورهايی است که در تابع يا هر تابعی که آن تابع فراخوانی کرده است (يا توابعی که آن‌ها فراخوانی کرده‌اند، و همين‌طور ادامه دارد) اجرا شده‌اند.

KLEE آمارهای گوناگونی درباره اجرا ارائه می‌کند. آماری که اکنون به آن توجه داريم «Uncovered Instructions» (دستورهای پوشش‌نيافته) است، که نشان می‌دهد کدام توابع دستورهايی دارند که هرگز اجرا نشده‌اند. اگر اين آمار را انتخاب کنيد و فهرست توابع را دوباره بر اساس آن مرتب کنيد، بايد چيزی شبيه اين ببينيد:

توجه کنيد که همان‌طور که انتظار داريم، بيشتر دستورهای پوشش‌نيافته در کدهای کتابخانه‌ای هستند. با اين حال، اگر تابع __user_main را انتخاب کنيم، می‌توانيم کدی را که درون خودِ echo پوشش‌نيافته مانده است پيدا کنيم. در اين مورد، بيشتر دستورهای پوشش‌نيافته داخل يک دستور if بزرگ قرار دارند که با متغير do_v9 کنترل می‌شود. اگر کمی دقيق‌تر نگاه کنيد، می‌بينيد که اين يک فلک (flag) است که زمانی روی true قرار می‌گيرد که گزينه ‎e-‎ دو خط تيره (⁠-e⁠) به echo داده شود. دليل اين‌که KLEE هرگز اين بخش از کد را کاوش نکرد اين است که ما فقط يک آرگومان نمادين (symbolic) به برنامه داديم؛ رسيدن به اين بخش نيازمند خط فرمانی شبيه اين است:

				
					$ echo -e \a

يک نکته ظريف که هنگام تلاش برای درک اعداد KCachegrind بايد به آن توجه کرد اين است که اين اعداد رخدادهايی را شامل می‌شوند که در همه حالت‌ها (states) انباشته شده‌اند. برای نمونه، اين کد را در نظر بگيريد:

				
					Line 1:      a = 1;
Line 2:      if (...)
Line 3:        printf("hello\n");
Line 4:      b = c;

در يک برنامه معمولی، اگر عبارت خط ۱ فقط يک بار اجرا شود، آنگاه عبارت خط ۴ هم در بيشترين حالت می‌تواند فقط يک بار اجرا شود. اما وقتی KLEE يک برنامه را اجرا می‌کند، ممکن است در خط ۲ انشعاب بدهد و فرایندهای جداگانه‌ای بسازد. در چنين حالتی، خط ۴ ممکن است **بیشتر** از خط ۱ اجرا شود!

يک نکته سودمند ديگر: KLEE در واقع فايل run.istats را **به صورت دوره‌ای** هنگام اجرای برنامه می‌نويسد. اين يک روش برای نظارت بر وضعيت برنامه‌های طولانی‌مدت است (يک روش ديگر استفاده از ابزار klee-stats است).

گام هفت: بازپخش آزمون‌های توليدشده توسط KLEE

بياييد کمی از KLEE فاصله بگيريم و فقط به آزمون‌هايی نگاه کنيم که KLEE توليد کرده است. اگر داخل پوشه klee-last را نگاه کنيم، بايد ۲۵ فايل با پسوند ‎.ktest‎ ببينيم.

				
					src$ ls klee-last
assembly.ll	  test000004.ktest  test000012.ktest  test000020.ktest
info		  test000005.ktest  test000013.ktest  test000021.ktest
messages.txt	  test000006.ktest  test000014.ktest  test000022.ktest
run.istats	  test000007.ktest  test000015.ktest  test000023.ktest
run.stats	  test000008.ktest  test000016.ktest  test000024.ktest
test000001.ktest  test000009.ktest  test000017.ktest  test000025.ktest
test000002.ktest  test000010.ktest  test000018.ktest  warnings.txt
test000003.ktest  test000011.ktest  test000019.ktest

اين فايل‌ها شامل مقادير واقعی هستند که بايد برای داده‌های نمادين (symbolic) استفاده شوند تا مسيری که KLEE دنبال کرده است بازتوليد شود (چه برای به‌دست آوردن پوشش کد، چه برای بازتوليد يک باگ). آن‌ها همچنين شامل متاديتای اضافی هستند که توسط زمان‌اجرای POSIX توليد شده تا مشخص شود مقادير به چه چيزی مربوط‌ می‌باشند و نسخه زمان‌اجرای برنامه چيست. می‌توانيم محتويات يک فايل را به صورت جداگانه با استفاده از ابزار ktest-tool مشاهده کنيم:

در اين مورد، آزمون نشان می‌دهد که مقادير “\x00\x00\x00\x00” بايد به عنوان آرگومان اول داده شوند. با اين حال، فايل‌های ‎.ktest‎ معمولاً برای مشاهده مستقيم طراحی نشده‌اند. برای زمان‌اجرای POSIX، ما ابزار klee-replay را فراهم کرده‌ايم که می‌تواند فايل ‎.ktest‎ را بخواند و برنامه بومی (native) را اجرا کند، به طوری که به صورت خودکار داده‌های لازم برای بازتوليد مسيری که KLEE دنبال کرده است را به آن بدهد.

برای ديدن نحوه کار، به پوشه‌ای بازگرديد که در آن اجرايی‌های بومی را ساخته بوديم:

				
					src$ cd ..
obj-llvm$ cd ..
coreutils-6.11$ cd obj-gcov
obj-gcov$ cd src
src$ ls -l echo
-rwxrwxr-x 1 klee klee 135984 Nov 21 21:58 echo

برای استفاده از ابزار klee-replay، کافی است نام برنامه اجرایی (executable) که بايد اجرا شود و فايل ‎.ktest‎ که بايد استفاده شود را به آن بدهيم. آرگومان‌های برنامه، فايل‌های ورودی و غيره همگی از داده‌های موجود در فايل ‎.ktest‎ ساخته می‌شوند.

دو خط اول و آخر اينجا از خود ابزار klee-replay هستند. دو خط اول آزمون در حال اجرا و مقادير واقعی (concrete) آرگومان‌هایی که به برنامه داده می‌شوند را نشان می‌دهند (توجه کنيد که اين مقادير همان چيزی است که قبلاً در فايل ‎.ktest‎ ديديم). خط آخر وضعيت خروجی برنامه و زمان سپری شده برای اجرا را نشان می‌دهد.

همچنين می‌توانيم از ابزار klee-replay برای اجرای يک مجموعه آزمون به صورت پشت سر هم استفاده کنيم. بياييد اين کار را انجام دهيم و پوشش gcov را با اعدادی که از klee-stats به دست آورديم مقايسه کنيم:

عدد مربوط به echo.c در اينجا به طور قابل توجهی بالاتر از عدد klee-stats است، زيرا gcov فقط خطوط همان فايل را در نظر می‌گيرد و نه کل برنامه را. مانند KCachegrind، می‌توانيم فايل خروجي پوشش که توسط gcov توليد شده را بررسی کنيم تا دقيقاً ببينيم کدام خطوط پوشش داده شده‌اند و کدام‌ها نشده‌اند. در اينجا يک بخش از خروجي آمده است:

ستون سمت چپ شمارش دفعات اجرای هر خط را نشان می‌دهد؛ علامت – به اين معناست که خط شامل کد قابل اجرا نيست، و ##### نشان می‌دهد که خط هرگز پوشش داده نشده است. همان‌طور که می‌بينيد، خطوط پوشش‌نيافته در اينجا کاملاً مطابق با خطوط پوشش‌نيافته‌ای هستند که در KCachegrind گزارش شده‌اند.

قبل از آنکه به تست برنامه‌های پيچيده‌تر بپردازيم، بياييد مطمئن شويم که می‌توانيم پوشش مناسبی از برنامه ساده echo.c به‌دست آوريم. مشکل قبلی اين بود که داده‌های کافی نمادين (symbolic) نبودند؛ ارائه دو آرگومان نمادين به echo بايد برای پوشش کامل برنامه کافی باشد. می‌توانيم از گزينه -sym-args- در زمان‌اجرای POSIX برای ارسال چندين آرگومان استفاده کنيم. در ادامه، مراحل کار بعد از بازگشت به پوشه obj-llvm/src آمده است:

				
					src$ klee --only-output-states-covering-new --optimize --libc=uclibc --posix-runtime ./echo.bc --sym-args 0 2 4
...
KLEE: done: total instructions = 7611521
KLEE: done: completed paths = 10179
KLEE: done: generated tests = 57

فرمت گزينه sym-args– در واقع مشخص می‌کند حداقل و حداکثر تعداد آرگومان‌هایی که بايد داده شوند و طول هر آرگومان چه باشد. در اين مثال، sym-args 0 2 4– می‌گويد بين ۰ و ۲ آرگومان (شامل حداقل و حداکثر) داده شود، هر کدام با طول حداکثر چهار کاراکتر.

ما همچنين گزينه –only-output-states-covering-new را به خط فرمان KLEE اضافه کرديم. به طور پيش‌فرض، KLEE برای هر مسيري که کاوش می‌کند، آزمون توليد می‌کند. اين وقتی برنامه بزرگ می‌شود کمتر مفيد است، زيرا بسياری از آزمون‌ها در نهايت همان مسيرها را تمرين می‌کنند و محاسبه يا حتی اجرای مجدد هر کدام زمان‌بر است. استفاده از اين گزينه به KLEE می‌گويد که تنها برای مسيرهایی که برخی از دستورهای جديد را پوشش داده‌اند (يا با خطا مواجه شده‌اند) آزمون توليد کند. خطوط پايانی خروجي نشان می‌دهد که حتی اگر KLEE تقريباً ده هزار مسير را کاوش کرده باشد، تنها نياز به نوشتن ۵۷ آزمون داشته است.

اگر به پوشه obj-gcov/src بازگرديم و آخرين مجموعه آزمون‌ها را دوباره اجرا کنيم، سرانجام پوشش مناسبی از echo.c به‌دست می‌آوريم:

دليل نرسيدن به پوشش کامل ۱۰۰٪ خطوط به عنوان يک تمرين برای خواننده گذاشته شده است.

گام هشت: استفاده از zcov برای تحليل پوشش

برای ديدارسازی نتايج پوشش، ممکن است بخواهيد از ابزار [1]zcov استفاده کنيد.

[1] symbolic virtual machine

[2] built on

[3] bitcode

[4] emulation

3. منابع

				
					https://klee-se.org/releases/
https://klee-se.org/getting-involved/
https://klee-se.org/publications/
https://klee-se.org/docs/
https://klee-se.org/getting-started/
https://www.youtube.com/watch?v=z6bsk-lsk1Q
https://www.youtube.com/watch?v=BDvNDw2jsSs&amp;t=1498s
https://github.com/klee/klee/tree/v3.1
https://github.com/stp/stp/releases/tag/2.3.3
https://klee-se.org/releases/docs/v3.1/build-llvm13/

راه اندازی آزمایشگاه Symbolic Exection توسط klee

Symbolic Exection Lab with klee