KLEE для C++ кода, который использует pthreads

Question

Я новичок, пытающийся использовать KLEE. Я использую автономный пакет KLEE для программы на C++, которая использует pthreads. Я сгенерировал.o файл и использовал KLEE со следующей опцией

klee --libc=uclibc --posix-runtime test.o

Но я вижу, что получаю предупреждение

KLEE: NOTE: Using model:
/home/pgbovine/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca

KLEE: output directory = "klee-out-4"
KLEE: WARNING: undefined reference to function: klee_get_valuel
KLEE: WARNING: undefined reference to function: pthread_create
KLEE: WARNING: undefined reference to function: pthread_exit
KLEE: WARNING: undefined reference to function: pthread_join
KLEE: WARNING: executable has module level assembly (ignoring)
KLEE: WARNING: calling external: syscall(54, 0, 21505, 571522624)
KLEE: WARNING: calling __user_main with extra arguments.
KLEE: WARNING: calling external: pthread_create(571589384, 0, 563903904, 571574176)
0  klee 0x08965ab8
[pid  1846] +++ killed by SIGSEGV +++

+++ killed by SIGSEGV +++
Segmentation fault

Использование klee в файле.bc также дает мне тот же результат.

Я не уверен, почему я получаю неопределенную ссылку на функции pthread. Я не уверен, правильно ли используются библиотеки для pthreads. Есть ли способ обеспечить это? Использование llvm-ld также не помогает.

Ниже приведена команда llvm-ld, которую я использовал

 llvm-ld tests.bc -l=/usr/lib/libpthread.a

Я не уверен, почему там происходит ошибка сегментации. Программа работает нормально, когда я обычно компилирую программы с g++ и запустите исполняемый файл.

Может кто-нибудь сказать мне, где я иду не так?

Answer 1

Проблема в том, что в Klee нет поддержки pthread. Следовательно, когда вы звоните pthread_create()Клее не ответит на это (вот почему вы видите KLEE: WARNING: calling external: pthread_create). В этом случае Klee потерпит крах из-за этой ошибки.

Answer 2

Если вы хотите использовать функцию pthread в KLEE, вы можете изменить исходный код KLEE, чтобы имитировать выполнение многопоточности.
В KLEE есть структура данных "ExecutionState", и когда вы создаете поток в пользовательском коде, вы можете соответственно создать ExecutionState в KLEE и установить "pc" для ExecutionState с помощью функции потока. Таким образом, вы можете перезаписать функции pthread в KLEE и перехватить вызов функции pthread с помощью пользовательского кода в функции executeInstruction в Executor.cpp.
Чтобы симулировать выполнение многопоточности, вы должны изменить искатель KLEE, который используется для выбора состояния для выполнения из всего вектора ExecutionState.
Так что это тяжелая работа.

Answer 3

Начиная с 2010 года базовая версия KLEE не поддерживает никакой формы параллелизма, включая pthread. Но у Раймондаса Саснаускаса (rwth-aachen) есть информация о проекте dslab из EPFL:

https://mailman.cs.umd.edu/pipermail/otter-dev/2010-December/000435.html

Текущая версия KLEE не поддерживает
параллелизм - вы должны реализовать / смоделировать его самостоятельно. Тем не менее, люди из EPFL уже внедрили pthread
поддержка в качестве расширения для KLEE и опубликовал хорошую статью о
Эта тема:

http://dslab.epfl.ch/pubs/esd

Есть архивная ссылка: http://web.archive.org/web/20100516044002/http://dslab.epfl.ch/pubs/esd"Синтез выполнения: методика автоматической отладки программного обеспечения", Кристиан Замфир и Джордж Кандея. Proc. 5-я Европейская конференция ACM SIGOPS/EuroSys по компьютерным системам (EuroSys), Париж, Франция, апрель 2010 г.

В 2013 году Кристиан Кадар опубликовал еще одну публикацию http://mailman.ic.ac.uk/pipermail/klee-dev/2013-January/000031.html которой отмечалось, что KLEE не поддерживает pthreads. Cloud9 Расширение KLEE может обрабатывать pthreads:

В настоящее время KLEE имеет ограниченную поддержку C++ и не поддерживает pthreads. Однако существуют определенные расширения для KLEE, которые обрабатывают эти аспекты, например, KLOVER для C++ и Cloud9 для pthreads. Посмотрите на http://klee.llvm.org/Publications.html для получения дополнительной информации.