sea dsa
1.0.0
SeaDsa -это контекстный, полезный и массив, основанный на объединении, основанный на точках точек, для биткода LLVM, вдохновленного DSA. SeaDsa на порядок более масштабируемый и точный, чем Dsa , и предыдущей реализации SeaDsa благодаря улучшению обработки чувствительности к контексту, добавлению частичной чувствительности потока и типовой осведомленности.
Хотя SeaDsa может проанализировать произвольный биткод LLVM, он был адаптирован для использования в программе проверки программ C/C ++. Его можно использовать в качестве автономного инструмента или вместе с структурой проверки Сихорна и его анализом.
Эта ветвь поддерживает LLVM 14.
SeaDsa написан в C ++ и использует библиотеку Boost. Основные требования:
Чтобы запустить тесты, установите следующие пакеты:
sudo pip install lit OutputChecksudo easy_install networkxsudo apt-get install libgraphviz-devsudo easy_install pygraphvizGraph , Cell и Node , определены в include/Graph.hh и src/Graph.cc .include/Local.hh и src/DsaLocal.cc .include/BottomUp.hh и src/DsaBottomUp.cc .include/TopDown.hh и src/DsaTopDown.cc .include/Cloner.hh и src/Clonner.cc .include/FieldType.hh , include/TypeUtils.hh , src/FieldType.cc и src/TypeUtils.cc .include/AllocWrapInfo.hh и src/AllocWrapInfo.cc . Инструкции по запуску контрольных показателей программы вместе с рецептами создания реальных проектов и наших результатов можно найти в Extras Tea-DSA-EXTRAS.
SeaDsa содержит два каталога: include и src . Поскольку SeaDsa анализирует биткод LLVM, файлы заголовков LLVM и библиотеки должны быть доступны при создании с SeaDsa .
Если ваш проект использует cmake , вам просто нужно добавить в CMakeLists.txt вашего проекта.txt:
include_directories(seadsa/include)
add_subdirectory(seadsa)
Если вы уже установили llvm-14 на свою машину:
mkdir build && cd build
cmake -DCMAKE_INSTALL_PREFIX=run -DLLVM_DIR=__here_llvm-14__/share/llvm/cmake ..
cmake --build . --target install
В противном случае:
mkdir build && cd build
cmake -DCMAKE_INSTALL_PREFIX=run ..
cmake --build . --target install
Чтобы запустить тесты:
cmake --build . --target test-sea-dsa
Рассмотрим программу C, называемую tests/c/simple.c :
#include <stdlib.h>
typedef struct S {
int * * x ;
int * * y ;
} S ;
int g ;
int main ( int argc , char * * argv ){
S s1 , s2 ;
int * p1 = ( int * ) malloc ( sizeof ( int ));
int * q1 = ( int * ) malloc ( sizeof ( int ));
s1 . x = & p1 ;
s1 . y = & q1 ;
* ( s1 . x ) = & g ;
return 0 ;
} Генерировать биткод:
clang -O0 -c -emit-llvm -S tests/c/simple.c -o simple.ll
Опция -O0 используется для отключения оптимизации кланг. В целом, это хорошая идея, чтобы обеспечить оптимизацию Clang. Тем не менее, для тривиальных примеров, таких как simple.c , Clang слишком много упрощает, поэтому ничего полезного не наблюдается. Опции -c -emit-llvm -S генерируют биткод в формате, читаемого на человеке.
Запустите sea-dsa на биткоде и распечатайте графики памяти в формат DOT:
seadsa -sea-dsa=butd-cs -sea-dsa-type-aware -sea-dsa-dot simple.ll
Опции -sea-dsa=butd-cs -sea-dsa-type-aware включите анализ, реализованный в нашей статье FMCAD'19 (см. Ссылки). Эта команда будет генерировать файл FUN.mem.dot для каждой функции FUN в программе BitCode. В нашем случае единственная функция является main , и, таким образом, есть один файл с именем main.mem.dot . Файл генерируется в текущем каталоге. Если вы хотите сохранить файлы .dot в другом DIR DIRECTORY, добавьте опцию -sea-dsa-dot-outdir=DIR
Визуализировать main.mem.dot , преобразив его в файл pdf :
dot -Tpdf main.mem.dot -o main.mem.pdf
open main.mem.pdf // replace with you favorite pdf viewer
В нашей модели памяти значение указателя представлено ячейкой , которая является парой объекта памяти и смещения. Объекты памяти представлены как узлы на графике памяти. Кренки находятся между ячейками.
Каждое поле узла представляет ячейку (т.е. смещение в узле). Например, поля узла <0,i32**> и <8,i32**> Указаны на %6 и %15 , соответственно, являются двумя разными ячейками из одного и того же объекта памяти. Поле <8,i32**> представляет ячейку в смещении 8 в соответствующем объекте памяти, а его тип i32** . Черные края представляют отношения между клетками. Они помечены числом, которое представляет собой смещение в узле назначения. Синие края соединяют формальные параметры функции с ячейкой. Фиолетовые края соединяют переменные указателя LLVM с клетками. У узлов могут быть такие маркеры, как S (стек, выделенная память), H (Heap выделяет память), M (модифицированная память), R (чтение памяти), E (извне распределенная память) и т. Д. Если узел является красным, то это означает, что анализ потерял чувствительность поля для этого узла. Метка {void} используется для обозначения того, что узел был выделен, но программа не использовалась.
sea-dsa также может разрешить косвенные звонки. Косвенное вызов - это вызов, когда Callee не известна статически. sea-dsa идентифицирует все возможные Callees непрямого вызова и генерирует график вызова LLVM в качестве вывода.
Рассмотрим этот пример в tests/c/complete_callgraph_5.c :
struct class_t ;
typedef int ( * FN_PTR )( struct class_t * , int );
typedef struct class_t {
FN_PTR m_foo ;
FN_PTR m_bar ;
} class_t ;
int foo ( class_t * self , int x )
{
if ( x > 10 ) {
return self -> m_bar ( self , x + 1 );
} else
return x ;
}
int bar ( class_t * self , int y ) {
if ( y < 100 ) {
return y + self -> m_foo ( self , 10 );
} else
return y - 5 ;
}
int main ( void ) {
class_t obj ;
obj . m_foo = & foo ;
obj . m_bar = & bar ;
int res ;
res = obj . m_foo ( & obj , 42 );
return 0 ;
}Введите команды:
clang -c -emit-llvm -S tests/c/complete_callgraph_5.c -o ex.ll
sea-dsa --sea-dsa-callgraph-dot ex.ll
Он генерирует файл .dot callgraph.dot в текущем каталоге. Опять же, файл .dot может быть преобразован в файл .pdf и открыт с помощью команд:
dot -Tpdf callgraph.dot -o callgraph.pdf
open callgraph.pdf
sea-dsa также может распечатать некоторые статистические данные о процессе разрешения графа вызовов (обратите внимание, что вам необходимо позвонить clang с -g для печати файла, строки и информации о столбцах):
sea-dsa --sea-dsa-callgraph-stats ex.ll
=== Sea-Dsa CallGraph Statistics ===
** Total number of indirect calls 0
** Total number of resolved indirect calls 3
%16 = call i32 %12(%struct.class_t* %13, i32 %15) at tests/c/complete_callgraph_5.c:14:12
RESOLVED
Callees:
i32 bar(%struct.class_t*,i32)
%15 = call i32 %13(%struct.class_t* %14, i32 10) at tests/c/complete_callgraph_5.c:23:16
RESOLVED
Callees:
i32 foo(%struct.class_t*,i32)
%11 = call i32 %10(%struct.class_t* %2, i32 42) at tests/c/complete_callgraph_5.c:36:9
RESOLVED
Callees:
i32 foo(%struct.class_t*,i32)
Семантика внешних вызовов указана может быть определена, написав обертку, которая вызывает любую из этих функций, определенных в seadsa/seadsa.h :
extern void seadsa_alias(const void *p, ...);extern void seadsa_collapse(const void *p);extern void seadsa_mk_seq(const void *p, unsigned sz); seadsa_alias объединяет все ячейки аргумента, seadsa_collapse говорит sea-dsa обрушиться (то есть потерю чувствительности к полю), ячейка, указанная на p , и seadsa_mk_seq говорит sea-dsa отметить в качестве последовательности , указанный на p Size sz .
Например, рассмотрим внешний вызов foo определенный следующим образом:
extern void* foo(const void*p1, void *p2, void *p3);
Предположим, что возвращенный указатель должен быть объединен для p2 , но не для p1 . Кроме того, мы хотели бы разрушить ячейку, соответствующую p3 . Затем мы можем заменить вышеуказанный прототип foo на следующее определение:
#include "seadsa/seadsa.h"
void* foo(const void*p1, void *p2, void*p3) {
void* r = seadsa_new();
seadsa_alias(r,p2);
seadsa_collapse(p3);
return r;
}
«Контекстно-чувствительная модель памяти для проверки программ C/C ++» от A. Gurfinkel и Ja Navas. В SAS'17. (Бумага) | (Слайды)
«Анализ указателей, основанный на объединении, без переживания» Дж. Кудерски, Дж. Наваса и А. Гурфинкеля. В FMCAD'19. (Бумага)
