sea dsa
1.0.0
SeaDsa es un análisis de puntos To basado en la unificación de contexto, de campo, y matriz para el código de bits LLVM inspirado en DSA. SeaDsa es un orden de magnitud más escalable y preciso que Dsa y una implementación previa de SeaDsa gracias al manejo mejorado de la sensibilidad del contexto, la adición de sensibilidad al flujo parcial y la conciencia de tipo.
Aunque SeaDsa puede analizar el código de bits LLVM arbitrario, se ha adaptado para su uso en la verificación del programa de los programas C/C ++. Se puede usar como una herramienta independiente o junto con el marco de verificación de Seahorn y sus análisis.
Esta rama admite LLVM 14.
SeaDsa está escrito en C ++ y usa la biblioteca Boost. Los principales requisitos son:
Para ejecutar pruebas, instale los siguientes paquetes:
sudo pip install lit OutputChecksudo easy_install networkxsudo apt-get install libgraphviz-devsudo easy_install pygraphvizGraph , Cell y Node , se definen en include/Graph.hh y src/Graph.cc .include/Local.hh y src/DsaLocal.cc .include/BottomUp.hh y src/DsaBottomUp.cc .include/TopDown.hh y src/DsaTopDown.cc .include/Cloner.hh y src/Clonner.cc .include/FieldType.hh , include/TypeUtils.hh , src/FieldType.cc y src/TypeUtils.cc .include/AllocWrapInfo.hh y src/AllocWrapInfo.cc . Las instrucciones sobre la ejecución de puntos de referencia de verificación del programa, junto con recetas para construir proyectos del mundo real y nuestros resultados, se pueden encontrar en Tea-Dsa-Extras.
SeaDsa contiene dos directorios: include y src . Dado que SeaDsa analiza el código de bits LLVM, los archivos y bibliotecas de encabezado LLVM deben ser accesibles al construir con SeaDsa .
Si su proyecto usa cmake , solo necesita agregar CMakeLists.txt de su proyecto.txt:
include_directories(seadsa/include)
add_subdirectory(seadsa)
Si ya instaló llvm-14 en su máquina:
mkdir build && cd build
cmake -DCMAKE_INSTALL_PREFIX=run -DLLVM_DIR=__here_llvm-14__/share/llvm/cmake ..
cmake --build . --target install
De lo contrario:
mkdir build && cd build
cmake -DCMAKE_INSTALL_PREFIX=run ..
cmake --build . --target install
Para ejecutar pruebas:
cmake --build . --target test-sea-dsa
Considere un programa C llamado 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 ;
} Genere un código de bits:
clang -O0 -c -emit-llvm -S tests/c/simple.c -o simple.ll
La opción -O0 se usa para deshabilitar las optimizaciones de clang. En general, es una buena idea habilitar las optimizaciones de Clang. Sin embargo, para ejemplos triviales como simple.c , Clang simplifica demasiado, por lo que no se observaría nada útil. Las opciones -c -emit-llvm -S generan bitcode en formato legible por humanos.
Ejecute sea-dsa en el código de bits e imprima los gráficos de memoria en formato DOT:
seadsa -sea-dsa=butd-cs -sea-dsa-type-aware -sea-dsa-dot simple.ll
Las opciones -sea-dsa=butd-cs -sea-dsa-type-aware habilitan el análisis implementado en nuestro documento FMCAD'19 (ver referencias). Este comando generará un archivo FUN.mem.dot para cada función FUN en el programa BitCode. En nuestro caso, la única función es main y, por lo tanto, hay un archivo llamado main.mem.dot . El archivo se genera en el directorio actual. Si desea almacenar los archivos .dot en un directorio de directorio diferente DIR agregue la opción -sea-dsa-dot-outdir=DIR
Visualice main.mem.dot transformándolo en un archivo pdf :
dot -Tpdf main.mem.dot -o main.mem.pdf
open main.mem.pdf // replace with you favorite pdf viewer
En nuestro modelo de memoria, un valor de puntero está representado por una celda que es un par de objeto de memoria y desplazamiento. Los objetos de memoria se representan como nodos en el gráfico de memoria. Los bordes están entre células.
Cada campo de nodo representa una celda (es decir, un desplazamiento en el nodo). Por ejemplo, los campos de nodo <0,i32**> y <8,i32**> señalados por %6 y %15 , respectivamente, son dos celdas diferentes del mismo objeto de memoria. El campo <8,i32**> representa la celda en el desplazamiento 8 en el objeto de memoria correspondiente y su tipo es i32** . Los bordes negros representan puntos hasta las relaciones entre las células. Están etiquetados con un número que representa el desplazamiento en el nodo de destino. Los bordes azules conectan los parámetros formales de la función con una celda. Púrpura Bordes conectan variables de puntero LLVM con celdas. Los nodos pueden tener marcadores como S (memoria asignada de pila), H (memoria de asignación de pistos), M (memoria modificada), R (memoria de lectura), E (memoria asignada externamente), etc. Si un nodo es rojo, entonces significa que el análisis perdió la sensibilidad de campo para ese nodo. La etiqueta {void} se usa para denotar que el nodo ha sido asignado, pero el programa no lo ha utilizado.
sea-dsa también puede resolver llamadas indirectas. Una llamada indirecta es una llamada donde la calle no se conoce estáticamente. sea-dsa identifica todas las calles posibles de una llamada indirecta y genera un gráfico de llamadas LLVM como salida.
Considere este ejemplo en 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 ;
}Escriba los comandos:
clang -c -emit-llvm -S tests/c/complete_callgraph_5.c -o ex.ll
sea-dsa --sea-dsa-callgraph-dot ex.ll
Genera un archivo .dot llamado callgraph.dot en el directorio actual. Nuevamente, el archivo .dot se puede convertir en un archivo .pdf y abrir con los comandos:
dot -Tpdf callgraph.dot -o callgraph.pdf
open callgraph.pdf
sea-dsa también puede imprimir algunas estadísticas sobre el proceso de resolución de gráficos de llamadas (tenga en cuenta que debe llamar clang con -g para imprimir información, línea e información de columna):
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)
La semántica del puntero de las llamadas externas se puede definir escribiendo un envoltorio que llama a cualquiera de estas funciones definidas en 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 unifica las celdas de todos los argumentos, seadsa_collapse le dice sea-dsa que colapsen (es decir, pérdida de sensibilidad al campo) la celda apuntada por p , y seadsa_mk_seq le dice a sea-dsa que marque como secuencia el nodo apuntado por p con el tamaño sz .
Por ejemplo, considere una llamada externa foo definida de la siguiente manera:
extern void* foo(const void*p1, void *p2, void *p3);
Supongamos que el puntero devuelto debe unificarse a p2 pero no a p1 . Además, nos gustaría colapsar la celda correspondiente a p3 . Luego, podemos reemplazar el prototipo anterior de foo con la siguiente definición:
#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;
}
"Un modelo de memoria sensible al contexto para la verificación de los programas C/C ++" por A. Gurfinkel y JA Navas. En Sas'17. (Papel) | (Diapositivas)
"Análisis de puntero basado en la unificación sin sobrevaltar" por J. Kuderski, JA Navas y A. Gurfinkel. En fmcad'19. (Papel)
