seahorn
v0.1.0 Release (SV-COMP'16)
Seahorn adalah kerangka analisis otomatis untuk bahasa berbasis LLVM. Versi ini dikompilasi terhadap LLVM 14.
Beberapa fitur yang didukung adalah
Seahorn dikembangkan terutama sebagai kerangka kerja untuk melakukan penelitian dalam verifikasi otomatis. Kerangka kerja menyediakan banyak komponen yang dapat disatukan dengan berbagai cara. Namun, ini bukan alat analisis statis "out-of-the-box".
Banyak alat dan contoh analisis dilengkapi dengan kerangka kerja. Kami terus mencari aplikasi baru dan memberikan dukungan kepada pengguna baru. Untuk informasi lebih lanjut tentang apa yang terjadi, periksa blog kami (jarang diperbarui).
Seahorn didistribusikan di bawah lisensi BSD yang dimodifikasi. Lihat lisensi.txt untuk detailnya.
Seahorn menyediakan skrip Python yang disebut sea untuk berinteraksi dengan pengguna. Diberikan program C yang dianotasi dengan pernyataan, pengguna hanya perlu mengetik: sea pf file.c
Hasil dari sea-pf adalah unsat jika semua pernyataan berlaku, sat jika ada pernyataan yang dilanggar.
Opsi pf memberi tahu Seahorn untuk menerjemahkan file.c ke dalam kode bitcode LLVM, menghasilkan satu set kondisi verifikasi (VC), dan akhirnya, menyelesaikannya. Pemecah back-end utama adalah spacer.
Perintah yang disediakan pf , antara lain, opsi berikut:
--show-invars : Tampilan invarian yang dihitung jika jawabannya unsat .
--cex=FILE : Menyimpan contoh kontra dalam FILE jika jawabannya sat .
-g : Kompilasi dengan informasi debug untuk contoh tandingan yang lebih dapat dilacak.
--step=large : Pengkodean Langkah Besar. Setiap hubungan transisi sesuai dengan fragmen bebas loop.
--step=small : Small-Step Encoding. Setiap hubungan transisi sesuai dengan blok dasar.
--track=reg : model (integer) register saja.
--track=ptr : model register dan pointer (tetapi bukan konten memori)
--track=mem : model skalar, pointer, dan konten memori
--inline : inline program sebelum verifikasi
--crab : Suntikan invarian dalam spacer yang dihasilkan oleh alat berbasis interpretasi abstrak kepiting. Baca di sini untuk detail tentang semua opsi kepiting (awalan --crab ). Anda dapat melihat invarian mana yang disimpulkan oleh kepiting dengan mengetik opsi --log=crab .
--bmc : Gunakan mesin BMC.
sea pf adalah pipa yang menjalankan beberapa perintah. Bagian individu dari pipa dapat dijalankan secara terpisah juga:
sea fe file.c -o file.bc : Seahorn Frontend menerjemahkan program C ke dalam bitcode LLVM yang dioptimalkan termasuk transformasi campuran -sisik.
sea horn file.bc -o file.smt2 : Seahorn menghasilkan kondisi verifikasi dari file.bc dan mengeluarkannya ke dalam format SMT -LIB V2. Pengguna dapat memilih antara gaya penyandian yang berbeda dengan beberapa tingkat presisi dengan menambahkan:
--step={small,large,fsmall,flarge} Di mana small adalah pengkodean langkah kecil, large adalah pengkodean blok-besar, fsmall adalah pengkodean langkah kecil yang menghasilkan klausa tanduk datar (yaitu, menghasilkan sistem transisi dengan hanya satu predikat), dan flarge : blok-besar encoding yang menghasilkan klaus yang menghasilkan klaus datar.
--track={reg,ptr,mem} di mana reg hanya model integer skalar, model ptr reg Pointer Address, dan mem Model ptr dan konten memori.
sea smt file.c -o file.smt2 : menghasilkan CHC dalam format SMT -LIB2. Adalah alias untuk sea fe diikuti dengan sea horn . Komando sea pf adalah alias untuk sea smt --prove .
sea clp file.c -o file.clp : menghasilkan CHC dalam format CLP.
sea lfe file.c -o file.ll : Menjalankan Legacy Front -End
Untuk melihat semua perintah, ketik sea --help . Untuk melihat opsi untuk setiap perintah individu CMD (misalnya, horn ), ketik sea CMD --help (misalnya, sea horn --help ).
Seahorn tidak menggunakan kepiting secara default. Untuk mengaktifkan kepiting, tambahkan opsi --crab ke perintah sea .
Interpreter abstrak secara default intra-prosedural dan menggunakan domain zona sebagai domain abstrak numerik. Opsi default ini harus cukup untuk pengguna normal. Untuk pengembang, jika Anda ingin menggunakan domain abstrak lainnya, Anda perlu:
cmake -DCRAB_USE_LDD=ON -DCRAB_USE_ELINA=ONsea dengan opsi --crab-dom=DOM di mana DOM bisa:int untuk intervalterm-int untuk interval dengan fungsi yang tidak ditafsirkanboxes : untuk interval disjungtifoct untuk Oktagonpk untuk polyhedra Untuk menggunakan analisis antar-prosedural kepiting, Anda perlu menjalankan sea dengan opsi --crab-inter
Secara default, interpreter abstrak hanya alasan tentang variabel skalar (IE, register LLVM). Jalankan sea dengan opsi --crab-track=mem --crab-singleton-aliases=true untuk alasan tentang konten memori.
Kepiting sebagian besar tidak sensitif pada jalur sementara spacer, pemecah klausa tanduk kami, peka terhadap jalur. Meskipun analisis yang tidak sensitif jalur lebih efisien, sensitivitas jalur biasanya diperlukan untuk membuktikan properti yang menarik. Ini memotivasi keputusan kami untuk menjalankan kepiting pertama (jika opsi --crab ) dan kemudian meneruskan invarian yang dihasilkan ke spacer. Saat ini ada dua cara bagi spacer untuk menggunakan invarian yang dihasilkan oleh kepiting. Opsi sea --horn-use-invs=VAL memberi tahu spacer cara menggunakan invarian itu:
VAL sama dengan bg maka invarian hanya digunakan untuk membantu spacer dalam membuktikan lemma bersifat induktif.VAL sama untuk always maka perilaku tersebut mirip dengan bg tetapi juga invarian juga digunakan untuk membantu spacer memblokir contoh tandingan. Nilai defaultnya adalah bg . Tentu saja, jika kepiting dapat membuktikan bahwa program ini aman maka spacer tidak dikenakan dalam biaya tambahan.
Properti diasumsikan sebagai pernyataan. Seahorn menyediakan perintah pernyataan statis, seperti sassert diilustrasikan dalam contoh berikut
/* verification command: sea pf --horn-stats test.c */
#include "seahorn/seahorn.h"
extern int nd ();
int main ( void ) {
int k = 1 ;
int i = 1 ;
int j = 0 ;
int n = nd ();
while ( i < n ) {
j = 0 ;
while ( j < i ) {
k += ( i - j );
j ++ ;
}
i ++ ;
}
sassert ( k >= n );
} Secara internal, Seahorn mengikuti konvensi SV-Comp tentang lokasi kesalahan pengkodean dengan panggilan ke fungsi kesalahan yang ditunjuk __VERIFIER_error() . Seahorn mengembalikan unsat ketika __VERIFIER_error() tidak terjangkau, dan program ini dianggap aman. Seahorn Returns sat ketika __VERIFIER_error() dapat dijangkau dan programnya tidak aman. Metode sassert() didefinisikan dalam seahorn/seahorn.h .
Selain membuktikan properti atau memproduksi contoh tandingan, kadang -kadang berguna untuk memeriksa kode yang dianalisis untuk mendapatkan gambaran kompleksitasnya. Untuk ini, Seahorn memberikan perintah sea inspect . Misalnya, diberikan program C ex.c :
sea inspect ex.c --sea-dsa=cs+t --mem-dot
Opsi --sea-dsa=cs+t memungkinkan konteks baru, analisis SEA-DSA yang sensitif-jenis yang dijelaskan dalam FMCAD19. Perintah ini menghasilkan file FUN.mem.dot untuk setiap fungsi FUN dalam program input. Untuk memvisualisasikan grafik fungsi utama, gunakan antarmuka Web Graphivz, atau perintah berikut:
$ dot -Tpdf main.mem.dot -o main.mem.pdfRincian lebih lanjut tentang grafik memori ada di repositori Seadsa: di sini.
Gunakan sea inspect --help untuk melihat semua opsi. Saat ini, opsi yang tersedia adalah:
sea inspect --profiler mencetak jumlah fungsi, blok dasar, loop, dll.sea inspect --mem-callgraph-dot Cetakan untuk dot grafik panggilan yang dibangun oleh Seadsa.sea inspect --mem-callgraph-stats mencetak ke output standar beberapa statsik tentang konstruksi grafik panggilan yang dilakukan oleh Seadsa.sea inspect --mem-smc-stats mencetak jumlah akses memori yang dapat terbukti aman oleh Seadsa.Cara termudah untuk memulai dengan Seahorn adalah melalui distribusi Docker.
$ docker pull seahorn/seahorn-llvm10:nightly
$ docker run --rm -it seahorn/seahorn-llvm10:nightly Mulailah dengan menjelajahi apa yang dapat dilakukan perintah sea :
$ sea --help
$ sea pf --help Tag nightly secara otomatis disegarkan setiap hari dan berisi versi pengembangan terbaru. Kami mempertahankan semua tag lain (yang membutuhkan pembaruan manual) jarang. Periksa tanggal di Dockerhub dan mencatat masalah di GitHub jika terlalu basi.
Contoh tambahan dan opsi konfigurasi ada di blog. Blog jarang diperbarui. Secara khusus, perubahan opsi, fitur dihapus, hal -hal baru ditambahkan. Jika Anda menemukan masalah di blog, beri tahu kami. Kami setidaknya akan memperbarui posting blog untuk menunjukkan bahwa itu tidak diharapkan berfungsi dengan versi terbaru dari kode.
Anda juga dapat menginstal secara manual oleh:
Mengikuti instruksi di Docker File Dockerfile: docker/seahorn-builder.Dockerfile .
Jika ini tidak berhasil, jalankan:
$ wget https://apt.llvm.org/llvm.sh
$ chmod +x llvm.sh
$ sudo ./llvm.sh 14
$ apt download libpolly-14-dev && sudo dpkg --force-all -i libpolly-14-dev *3 perintah pertama akan menginstal llvm 14, tanggal 4 akan menginstal libpolly yang salah dihilangkan dari llvm 14 (tetapi termasuk dalam versi berikutnya)
Selanjutnya, ikuti instruksi di file Docker di atas
Informasi dari titik ini hanya untuk pengembang. Jika Anda ingin berkontribusi pada Seahorn, membangun alat Anda sendiri berdasarkan itu, atau hanya tertarik pada cara kerjanya di dalam, teruslah membaca.
Seahorn membutuhkan LLVM, Z3, dan Boost. Versi yang tepat dari perpustakaan terus berubah, tetapi CMake Craft digunakan untuk memeriksa bahwa versi yang tepat tersedia.
Untuk menentukan versi spesifik dari salah satu dependensi, gunakan biasanya <PackageName>_ROOT dan/atau <PackageName>_DIR (lihat find_package () untuk detailnya) variabel cmake.
Seahorn dipecah menjadi beberapa komponen yang hidup dalam repositori yang berbeda (di bawah organisasi Seahorn). Proses build secara otomatis memeriksa segala sesuatu yang diperlukan. Untuk instruksi build saat ini, periksa skrip CI.
Ini adalah langkah generik. Jangan gunakan itu. Baca terus untuk cara yang lebih baik:
cd seahorn ; mkdir build ; cd build (Direktori Build juga dapat berada di luar direktori sumber.)cmake -DCMAKE_INSTALL_PREFIX=run ../ (instal diperlukan! )cmake --build . --target extra && cmake .. (Klon Komponen yang tinggal di tempat lain)cmake --build . --target crab && cmake .. (Perpustakaan Kepiting Klon)cmake --build . --target install (Bangun dan instal semuanya di bawah run )cmake --build . --target test-all (Jalankan Tes)Catatan : Instal Target diperlukan agar tes berfungsi!
Untuk pengalaman pengembangan yang ditingkatkan:
clanglld Linkercompile_commands.json Di Linux, kami sarankan konfigurasi cmake berikut:
$ cd build
$ cmake -DCMAKE_INSTALL_PREFIX=run
-DCMAKE_BUILD_TYPE=RelWithDebInfo
-DCMAKE_CXX_COMPILER="clang++-14"
-DCMAKE_C_COMPILER="clang-14"
-DSEA_ENABLE_LLD=ON
-DCMAKE_EXPORT_COMPILE_COMMANDS=1
../
-DZ3_ROOT=<Z3_ROOT>
-DLLVM_DIR=<LLMV_CMAKE_DIR>
-GNinja
$ (cd .. && ln -sf build/compile_commands.json .)
di mana <Z3_ROOT adalah direktori yang mengandung distribusi biner Z3, dan LLMV_CMAKE_DIR adalah direktori yang mengandung LLVMConfig.cmake .
Opsi hukum lainnya untuk CMAKE_BUILD_TYPE adalah Debug dan Coverage . Perhatikan bahwa CMAKE_BUILD_TYPE harus kompatibel dengan yang digunakan untuk mengkompilasi LLVM . Secara khusus, Anda akan memerlukan Debug build LLVM untuk mengkompilasi SeaHorn dalam mode `debug **. Pastikan Anda memiliki banyak kesabaran, ruang disk, dan waktu jika Anda memutuskan untuk menempuh rute ini.
Atau, proyek ini dapat dikonfigurasi menggunakan preset CMake. Untuk melakukan ini, cukup jalankan perintah berikut:
$ cmake --preset < BUILD_TYPE > - < PRESET_NAME > Untuk mengonfigurasi cmake, di mana <BUILD_TYPE> adalah salah satu: Debug , RelWithDebInfo atau Coverage dan <PRESET_NAME> adalah preset yang ingin Anda gunakan. Preset yang saat ini tersedia adalah: jammy . Preset ini mengasumsikan bahwa Anda telah menginstal Z3 di /opt/z3-4.8.9 dan yices diinstal di /opt/yices-2.6.1 .
Ini juga akan memungkinkan proyek untuk dikonfigurasi dan dikompilasi dalam VS Code menggunakan ekstensi CMake Tools.
Jika Anda ingin menggunakan pengaturan kompilasi yang berbeda atau jika Anda memiliki Z3 atau Yices yang diinstal di direktori lain, Anda perlu membuat file CMakeUserPresets.json Anda sendiri dengan preset Anda sendiri.
Jangan sertakan -DSEA_ENABLE_LLD=ON . Kompiler default adalah dentang, jadi Anda mungkin tidak perlu mengaturnya secara eksplisit.
Seahorn menyediakan beberapa komponen yang secara otomatis dikloning dan dipasang melalui target extra . Komponen -komponen ini dapat digunakan oleh proyek lain di luar Seahorn.
SEA-DSA: git clone https://github.com/seahorn/sea-dsa.git
sea-dsa adalah analisis tumpukan berbasis DSA baru. Tidak seperti llvm-dsa , sea-dsa peka terhadap konteks dan oleh karena itu, partisi heap berbutir lebih halus dapat dihasilkan dengan adanya panggilan fungsi.
clam: git clone https://github.com/seahorn/crab-llvm.git
clam memberikan invarian induktif menggunakan teknik interpretasi abstrak untuk backend Seahorn lainnya.
LLVM-SHIEHORN: git clone https://github.com/seahorn/llvm-seahorn.git
llvm-seahorn menyediakan versi yang disesuaikan dengan verifikasi dari InstCombine dan IndVarSimplify LLVM pass serta llvm pass untuk mengubah nilai yang tidak terdefinisi menjadi panggilan nondeterministik, antara lain.
Seahorn tidak datang dengan versi dentangnya sendiri dan berharap menemukannya baik di direktori build ( run/bin ) atau di jalur. Pastikan versi dentang cocok dengan versi LLVM yang digunakan untuk mengkompilasi Seahorn (saat ini LLVM14). Cara termudah untuk memberikan versi dentang yang tepat adalah dengan mengunduhnya dari llvm.org, buka saja di suatu tempat dan buat tautan simbolis ke clang dan clang++ di run/bin .
$ cd seahorn/build/run/bin
$ ln -s < CLANG_ROOT > /bin/clang clang
$ ln -s < CLANG_ROOT > /bin/clang++ clang++ di mana <CLANG_ROOT> adalah lokasi di mana dentang dibongkar.
Infrastruktur pengujian tergantung pada beberapa paket Python. Ini memiliki dependensi sendiri. Jika Anda tidak dapat mengetahuinya, gunakan Docker sebagai gantinya.
$ pip install lit OutputCheck networkx pygraphviz Kami dapat menggunakan gcov dan lcov untuk menghasilkan informasi cakupan tes untuk Seahorn. Untuk membangun dengan cakupan yang diaktifkan, kita perlu menjalankan build di bawah direktori yang berbeda dan mengatur CMAKE_BUILD_TYPE ke Coverage selama konfigurasi cmake.
Contoh Langkah untuk Menghasilkan Laporan Cakupan untuk Target test-opsem :
mkdir coverage; cd coverage Buat dan Masukkan Direktori Bangun Cakupancmake -DCMAKE_BUILD_TYPE=Coverage <other flags as you wish> ../cmake --build . --target test-opsem Run Tes Opsem, Sekarang file .gcda dan .gcno harus dibuat di direktori CMakeFiles yang sesuailcov -c --directory lib/seahorn/CMakeFiles/seahorn.LIB.dir/ -o coverage.info mengumpulkan data cakupan dari modul yang diinginkan, jika clang digunakan sebagai kompiler alih -alih gcc , buat skrip bash llvm-gcov.sh : #! /bin/bash
exec llvm-cov gcov " $@ " $ chmod +x llvm-gcov.sh lalu tambahkan --gcov-tool <path_to_wrapper_script>/llvm-gcov.sh ke perintah lcov -c ... 6. Ekstrak data dari direktori yang diinginkan dan hasilkan laporan HTML:
lcov --extract coverage.info " */lib/seahorn/* " -o lib.info
lcov --extract coverage.info " */include/seahorn/* " -o header.info
cat header.info lib.info > all.info
genhtml all.info --output-directory coverage_report Kemudian buka coverage_report/index.html di browser untuk melihat laporan cakupan
Juga lihat scripts/coverage untuk skrip yang digunakan oleh CI. Laporan Cakupan untuk Build Nightly tersedia di Codecov
Database Kompilasi untuk Proyek Seahorn dan semua sub -proyeknya dihasilkan menggunakan -DCMAKE_EXPORT_COMPILE_COMMANDS=ON Option for cmake .
Cara mudah untuk mendapatkan pengindeksan kode untuk bekerja dengan dukungan database kompilasi adalah dengan menautkan file compilation_database.json ke direktori proyek utama dan mengikuti instruksi khusus untuk editor Anda.
lsp-ui dengan clangd yang tersedia di Spacemacs mengembangkan cabang Untuk panduan terperinci untuk alur kerja jarak jauh dengan konfigurasi clion pemeriksaan clion.
Gunakan garpu mainframer kami. Jangan lewatkan contoh konfigurasi.
