seahorn下载 - seahorn源代码下载

seahorn

其他类别

v0.1.0 Release (SV-COMP'16)

下载

关于

Seahorn是基于LLVM的语言的自动分析框架。此版本针对LLVM 14编译。

一些支持的功能是

基于抽象解释的静态分析
基于统一的上下文敏感指针分析
基于SMT的有限模型检查（即符号执行）
基于CHC的软件模型检查（即不变推理）
可执行的反例（即，没有报告，只是错误！）

Seahorn主要是用于进行自动验证研究的框架。该框架提供了许多可以通过多种方式组合在一起的组件。但是，这不是“开箱即用”的静态分析工具。

框架提供了许多分析工具和示例。我们一直在寻找新的应用程序，并为新用户提供支持。有关正在发生的事情的更多信息，请查看我们（不经常更新的）博客。

执照

Seahorn根据修改后的BSD许可分发。有关详细信息，请参见License.txt。

介绍

Seahorn提供了一个名为sea的Python脚本，可以与用户互动。给定一个带有断言注释的C程序，用户只需要键入： sea pf file.c

如果所有断言持有所有断言，则sea-pf的结果是unsat sat如果违反了任何主张。

pf选项告诉Seahorn将file.c转换为LLVM比特码，生成一组验证条件（VCS），最后解决它们。主要的后端求解器是间隔者。

命令pf提供以下选项：

--show-invars ：如果答案是unsat则显示计算的不变性。
--cex=FILE ：如果答案是sat在FILE中存储一个反例。
-g ：与调试信息一起编译，以获取更多可跟踪的反例。
--step=large ：大型编码。每个过渡关系对应于无环的片段。
--step=small ：小步骤编码。每个过渡关系对应于一个基本块。
--track=reg ：模型（整数）仅注册。
--track=ptr ：模型寄存器和指针（但不是内存内容）
--track=mem ：模拟标量，指针和内存内容
--inline ：在验证之前将程序嵌入
--crab ：基于Crab Abstract-terpretation工具生成的spacer中的注入不变性。在此处阅读以获取有关所有螃蟹选项（前缀--crab ）的详细信息。您可以通过键入选项--log=crab来查看哪些不变性是由螃蟹推断出来的。
--bmc ：使用BMC引擎。

sea pf是运行多个命令的管道。管道的各个部分也可以单独运行：

sea fe file.c -o file.bc ：SeaHorn Frontend将C程序转换为优化的LLVM比特码，包括混合仪器转换。
sea horn file.bc -o file.smt2 ：SeaHorn从file.bc生成验证条件，并将其输出为SMT -LIB V2格式。用户可以通过添加以下精度的不同编码样式在不同的编码样式之间进行选择：
- --step={small,large,fsmall,flarge} ，其中small步骤编码， large是大量的编码， fsmall是小步骤编码生成平坦的号角条款（即，它仅生成一个具有一个谓词的过渡系统），而flarge ：Block-Large-Large编码生成平坦的角喇叭。
- --track={reg,ptr,mem}其中reg仅建模整数标量， ptr模型reg和指针地址，以及mem模型ptr和内存内容。
sea smt file.c -o file.smt2 ：以SMT -LIB2格式生成CHC。是sea fe的别名，然后是sea horn 。命令sea pf是sea smt --prove 。
sea clp file.c -o file.clp ：以CLP格式生成CHC。
sea lfe file.c -o file.ll ：运行遗产前端

要查看所有命令，请键入sea --help 。要查看每个单独命令CMD（例如， horn ）的选项，型sea CMD --help （例如， sea horn --help ）。

抽象解释的静态分析

使用螃蟹的诱导不变性推断

Seahorn默认情况下不使用螃蟹。要启用螃蟹，请将选项--crab添加到sea Command。

默认情况下，抽象解释器是过程内部的，它将区域域用作数值抽象域。对于普通用户，这些默认选项应该足够。对于开发人员，如果您想使用其他抽象域，则需要：

使用cmake选项编译-DCRAB_USE_LDD=ON -DCRAB_USE_ELINA=ON
带有选项的sea --crab-dom=DOM DOM在其中可能是：
- int间隔
- 具有未解释功能的间隔的term-int
- boxes ：用于分离的间隔
- 十月的oct
- pk POLEHEDRA的PK

要使用螃蟹术间分析，您需要使用选项运行sea --crab-inter

默认情况下，抽象解释器仅有关标量变量（即LLVM寄存器）的原因。与选项一起运行sea --crab-track=mem --crab-singleton-aliases=true thue of Memory内容的理由。

如何使用螃蟹在垫片中产生的不变性

螃蟹主要是对路径不敏感的，而我们的号角求解器Spacer对路径敏感。尽管不敏感的分析更有效，但通常需要路径敏感性才能证明感兴趣的特性。这激发了我们运行第一只螃蟹（如果选择--crab ）的决定，然后将生成的不变性传递给垫片。当前，垫片使用Crab生成的不变式有两种方法。 sea选项--horn-use-invs=VAL告诉spacer如何使用那些不变式：

如果VAL等于bg则仅使用不变性来帮助spacer证明引理是感应的。
如果VAL等于always ，则该行为与bg相似，但此外，不变性也可用于帮助spacer阻塞反例。

默认值为bg 。当然，如果螃蟹可以证明该程序是安全的，那么垫片不会以任何额外的费用产生。

属性规范

假定属性是断言。 Seahorn提供了静态断言命令sassert ，如下示例所示

 /* 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 );
}

在内部，SeaHorn遵循SV-Comp的规定编码错误位置，通过呼叫指定的错误函数__VERIFIER_error() 。当__VERIFIER_error()无法到达时，SeaHorn返回unsat ，并且该程序被认为是安全的。当__VERIFIER_error()到达且程序不安全时，Seahorn返回sat 。 sassert()方法定义在seahorn/seahorn.h中。

检查代码

除了证明属性或制作反例外，有时还要检查正在分析的代码以了解其复杂性是有用的。为此，Seahorn提供了指挥sea inspect 。例如，给定的C程序ex.c类型：

 sea inspect ex.c --sea-dsa=cs+t --mem-dot

选项--sea-dsa=cs+t可以实现FMCAD19中描述的新上下文，类型敏感的SEA-DSA分析。此命令为输入程序中的每个函数FUN生成一个FUN.mem.dot文件。要可视化主函数的图，请使用Web Graphivz接口或以下命令：

$ dot -Tpdf main.mem.dot -o main.mem.pdf

内存图的更多详细信息在Seadsa存储库中：此处。

使用sea inspect --help来查看所有选项。目前，可用选项是：

sea inspect --profiler打印功能，基本块，循环等的数量。
sea inspect --mem-callgraph-dot打印以dot格式，由Seadsa构建的呼叫图。
sea inspect --mem-callgraph-stats打印以标准输出一些有关Seadsa完成的呼叫图构造的Statstics。
sea inspect --mem-smc-stats打印了Seadsa可以证明可以证明的记忆访问的数量。

安装

开始使用Seahorn的最简单方法是通过Docker发行。

$ docker pull seahorn/seahorn-llvm10:nightly
$ docker run --rm -it seahorn/seahorn-llvm10:nightly

首先探索sea Command可以做什么：

$ sea --help
$ sea pf --help

nightly标签每天自动刷新，并包含最新的开发版本。我们很少维护所有其他标签（需要手动更新）。检查Dockerhub上的日期，并在Github上记录问题，以确定它们是否过时。

其他示例和配置选项在博客上。博客很少更新。特别是，选项更改，逐步淘汰功能，添加了新事物。如果您在博客中发现问题，请告诉我们。我们至少会更新博客文章，以表明它不会与最新版本的代码一起使用。

您也可以通过以下方式手动安装：

按照Docker文件Dockerfile中的说明： docker/seahorn-builder.Dockerfile 。

如果这不起作用，请运行：

$ 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个命令将安装LLVM 14，第四命令将安装LLVM 14省略的LIBPOLLY（但包含在后续版本中）

接下来，按照上面的Docker文件中的说明

开发人员的区域

此时的信息仅适用于开发人员。如果您想为Seahorn做出贡献，请基于它构建自己的工具，或者只是对其在内部工作方式感兴趣，请继续阅读。

汇编说明

Seahorn需要LLVM，Z3和Boost。库的确切版本不断变化，但Cmake Craft用于检查正确版本是否可用。

要指定任何依赖项的特定版本，请使用通常的<PackageName>_ROOT和/或<PackageName>_DIR （有关详细信息）CMAKE变量。

Seahorn被分成多个生活在不同存储库（在Seahorn组织下）的组件。构建过程会根据需要自动检查所有内容。对于当前的构建说明，请检查CI脚本。

这些是通用步骤。不要使用它们。以更好的方式阅读：

cd seahorn ; mkdir build ; cd build （构建目录也可以在源目录之外。）
cmake -DCMAKE_INSTALL_PREFIX=run ../ （需要安装！ ）
cmake --build . --target extra && cmake .. （在其他地方生活的克隆组件）
cmake --build . --target crab && cmake .. （克隆蟹库）
cmake --build . --target install （在run下构建和安装所有内容）
cmake --build . --target test-all （运行测试）

注意：测试工作需要安装目标！

更好的汇编说明

为了获得增强的发展经验：

使用clang
在Linux上，使用lld链接器
在发行版中包括调试符号
使用忍者
导出compile_commands.json

在Linux上，我们建议以下cmake配置：

 $ 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 .)

其中<Z3_ROOT是包含Z3二进制分布的目录，而LLMV_CMAKE_DIR是包含LLVMConfig.cmake的目录。

CMAKE_BUILD_TYPE的其他法律选择是Debug和Coverage 。请注意， CMAKE_BUILD_TYPE必须与用于编译LLVM cmake_build_type兼容。特别是，您将需要LLVM的Debug构建来以“调试**”模式编译SeaHorn 。确保您有足够的耐心，磁盘空间和时间，如果您决定走这条路线。

或者，可以使用CMAKE预设配置该项目。为此，只需运行以下命令：

$ cmake --preset < BUILD_TYPE > - < PRESET_NAME >

要配置cmake，其中<BUILD_TYPE>是： Debug ， RelWithDebInfo或Coverage之一， <PRESET_NAME>是您想要使用的预设。当前可用的预设是： jammy 。这些预设假设您已安装在/opt/z3-4.8.9中的Z3，并且安装在/opt/yices-2.6.1中的YICES。

这还将允许使用CMAKE工具扩展程序在VS代码中配置和编译该项目。

如果您想使用不同的汇编设置，或者您在任何其他目录中安装了Z3或YICE，则需要使用自己的预设制作自己的CMakeUserPresets.json文件。

在Mac上编译

请勿包括-DSEA_ENABLE_LLD=ON 。默认编译器是clang的，因此您可能无需明确设置它。

额外的目标

Seahorn提供了几个组件，它们通过extra目标自动克隆和安装。这些组件可以由Seahorn以外的其他项目使用。

SEA-DSA： git clone https://github.com/seahorn/sea-dsa.git
sea-dsa是一种新的基于DSA的堆分析。与llvm-dsa不同， sea-dsa是上下文敏感的，因此，可以在存在功能调用的情况下生成堆的细粒分区。
蛤： git clone https://github.com/seahorn/crab-llvm.git
clam使用抽象的解释技术为Seahorn的其余后端提供了诱导不变性。
llvm-seahorn： git clone https://github.com/seahorn/llvm-seahorn.git
llvm-seahorn提供了量身定制的InstCombine和IndVarSimplify LLVM通行证以及LLVM通行证的量身定制的版本，以将不确定的值转换为非确定呼叫等。

Seahorn不带有自己的Clang版本，并且希望在构建目录（ run/bin ）或路径中找到它。确保Clang的版本与用于编译Seahorn的LLVM的版本匹配（当前LLVM14）。提供正确版本的Clang的最简单方法是从llvm.org下载它，在某个地方打开它，并在run/bin中创建指向clang和clang++的符号链接。

$ cd seahorn/build/run/bin
$ ln -s < CLANG_ROOT > /bin/clang clang
$ ln -s < CLANG_ROOT > /bin/clang++ clang++

其中<CLANG_ROOT>是拆开包装的位置。

测试

测试基础架构取决于几个Python软件包。这些有自己的依赖性。如果您无法弄清楚它们，请改用Docker。

$ pip install lit OutputCheck networkx pygraphviz

覆盖范围

我们可以使用gcov和lcov来为Seahorn生成测试覆盖信息。要启用覆盖范围，我们需要在其他目录下运行构建，并将CMAKE_BUILD_TYPE设置为CMAKE配置期间的Coverage 。

用于生成test-opsem目标覆盖范围报告的示例步骤：

mkdir coverage; cd coverage创建并输入覆盖范围构建目录
cmake -DCMAKE_BUILD_TYPE=Coverage <other flags as you wish> ../
照常完成构建
cmake --build . --target test-opsem运行OPSEM测试，现在.gcda和.gcno文件应在相应的CMakeFiles目录中创建
lcov -c --directory lib/seahorn/CMakeFiles/seahorn.LIB.dir/ -o coverage.info从所需模块中收集覆盖范围数据，如果clang用作编译器而不是gcc ，请创建BASH脚本llvm-gcov.sh ：

 #! /bin/bash
exec llvm-cov gcov " $@ "

$ chmod +x llvm-gcov.sh

然后将--gcov-tool <path_to_wrapper_script>/llvm-gcov.sh附加到lcov -c ...命令。 6.从所需目录中提取数据并生成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

然后在浏览器中打开coverage_report/index.html以查看覆盖报告

另请参阅CI使用的脚本的scripts/coverage 。 Codecov提供了夜间构建的报道报告

代码索引

Seahorn项目及其所有子项目的编译数据库均使用-DCMAKE_EXPORT_COMPILE_COMMANDS=ON OPENT for cmake生成。

将代码索引与编译数据库支持一起使用的一种简单方法是将compilation_database.json文件链接到主要项目目录中，并遵循特定于编辑器的说明。

Clion-https://www.jetbrains.com/help/clion/compilation-database.html
vim（youcompleteme） - 说明
emacs-使用lsp-ui与clangd一起使用，该clangd可以在SpaceMacs开发分支

CLION的远程配置

有关CLION检查Clion-Configuration的远程工作流程的详细指南。

EMAC（和其他编辑器）的远程配置

使用我们的MainFramer叉。不要错过示例配置。

贡献者

Arie Gurfinkel
豪尔赫·纳瓦斯（Jorge Navas）
Temesghen Kahsai
Jakub Kuderski
纳姆·勒
查尔斯·雷（Charles Lei）
西安周
Siddharth Priya
伊莎贝尔·加西亚·克雷特拉斯
Yusen Su
给我发电子邮件，如果你的名字在这里

展开

附加信息

版本 v0.1.0 Release (SV-COMP'16)
类型其他类别
更新时间 2025-06-22
大小 2.14MB
来自于 Github

seahorn

关于

执照

介绍

抽象解释的静态分析

使用螃蟹的诱导不变性推断

如何使用螃蟹在垫片中产生的不变性

属性规范

检查代码

安装

开发人员的区域

汇编说明

更好的汇编说明

在Mac上编译

额外的目标

测试

覆盖范围

代码索引

CLION的远程配置

EMAC（和其他编辑器）的远程配置

贡献者

IDArling

hextor

intellij tai e

microavx

cwe_checker

pyt

chat.petals.dev

GPT Prompt Templates

GPTyped

IDArling

hextor

intellij tai e

Google Dorks

shepherd

mongo express