AliveToolkit/alive2

# Alive2  Alive2 由多个库和工具组成，用于分析和验证 LLVM 代码及其转换。 Alive2 包含以下库： * Alive2 IR * Symbolic executor (符号执行器) * LLVM → Alive2 IR converter (转换器) * Refinement check (改进检查，即优化验证器) * SMT abstraction layer (SMT 抽象层) 包含的工具： * Alive 直接替换工具 * 用于 clang 和 LLVM `opt` 的转换验证插件 * 独立转换验证工具：`alive-tv` ([在线版](https://alive2.llvm.org)) * 带有转换验证的 Clang 直接替换工具 (`alivecc` 和 `alive++`) * 精确 UB 的 LLVM IR 解释器 (`alive-exec`) 关于 Alive2 的技术介绍，请参阅 [我们要 PLDI 2021 提交的论文](https://web.ist.utl.pt/nuno.lopes/pubs/alive2-pldi21.pdf)。 ## 警告 Alive2 不支持过程间转换。如果在此类 pass 下运行，Alive2 可能会产生虚假的反例。 ## 前置条件 构建 Alive2 需要以下软件的最新版本： * [cmake](https://cmake.org) * [gcc](https://gcc.gnu.org)/[clang](https://clang.llvm.org) * [re2c](https://re2c.org/) * [Z3](https://github.com/Z3Prover/z3) * [LLVM](https://github.com/llvm/llvm-project) (可选) * [hiredis](https://github.com/redis/hiredis) (可选，用于缓存) ## 构建 ``` git clone git@github.com:AliveToolkit/alive2.git cd alive2 mkdir build cd build cmake -GNinja -DCMAKE_BUILD_TYPE=Release .. ninja ``` 如果 CMake 找不到 Z3 的包含目录（或者找到了错误的目录），请将 ``-DZ3_INCLUDE_DIR=/path/to/z3/include`` 和 ``-DZ3_LIBRARIES=/path/to/z3/lib/libz3.so`` 参数传递给 CMake。 ## 构建和运行转换验证 Alive2 的 `opt` 和 `clang` 转换验证需要构建启用了 RTTI 和异常的 LLVM。Alive2 的最新版本始终旨在针对 LLVM 的最新版本构建，使用 Github 上 LLVM 仓库的 main 分支。 LLVM 可以通过以下方式构建。 * 如果您的默认编译器是 `gcc`，您可能希望在 CMake 步骤中添加 `-DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++`。 * 可能不需要显式设置目标。 * `BUILD_SHARED_LIBS` 可能不是必需的，对于通常不使用该选项构建的 LLVM 分支，它可能会干扰 CMake 文件对 `USEDLIBS` 和 `LLVMLIBS` 以及可能的 `dd_llvm_target` 的使用。 * 要使用 Xcode 而不是 Ninja 进行构建，请在下面的 `cmake` 步骤中将 `-GNinja` 替换为 `-GXcode`，并附加 `-DLLVM_MAIN_SRC_DIR=~/llvm/llvm`。 * 可能需要在项目构建设置中禁用“Implicit Conversion to 32 Bit Type”的警告。 * Xcode 可能会将 `tv.dylib` 放置在不同的位置；从实际位置到结果错误消息中的位置创建一个符号链接可能会有所帮助。 ``` cd ~/llvm mkdir build cd build cmake -GNinja -DLLVM_ENABLE_RTTI=ON -DBUILD_SHARED_LIBS=ON -DCMAKE_BUILD_TYPE=Release -DLLVM_ENABLE_ASSERTIONS=ON -DLLVM_ENABLE_PROJECTS="llvm;clang" ../llvm ninja ``` 然后应按如下方式配置和构建 Alive2： ``` cd ~/alive2/build cmake -GNinja -DCMAKE_PREFIX_PATH=~/llvm/build -DBUILD_TV=1 -DCMAKE_BUILD_TYPE=Release .. ninja ``` 转换验证一个或多个转换 IR 文件的 LLVM pass： ``` ~/alive/build/alive-tv -passes=instcombine foo.ll ``` 或者使用 opt 包装器： ``` ~/alive2/build/opt-alive-test.sh -passes=instcombine foo.ll ``` 使用 lit 对单个 LLVM 单元测试进行转换验证： ``` ~/llvm/build/bin/llvm-lit -vv -Dopt=~/alive2/build/opt-alive.sh ~/llvm/llvm/test/Transforms/InstCombine/canonicalize-constant-low-bit-mask-and-icmp-sge-to-icmp-sle.ll ``` 输出应该是： ``` -- Testing: 1 tests, 1 threads -- PASS: LLVM :: Transforms/InstCombine/canonicalize-constant-low-bit-mask-and-icmp-sge-to-icmp-sle.ll (1 of 1) Testing Time: 0.11s Expected Passes : 1 ``` 要对所有 IR 级别转换的 LLVM 单元测试运行转换验证： ``` ~/llvm/build/bin/llvm-lit -s -Dopt=~/alive2/build/opt-alive.sh ~/llvm/llvm/test/Transforms ``` 我们每天在 LLVM 主分支上运行此命令，并在此处记录结果 [此处](https://web.ist.utl.pt/nuno.lopes/alive2/)。要在本地运行中检测不健全的转换： ``` grep -Fr "(unsound)" ~/alive2/build/logs/ ``` ## 作为 Clang 插件运行 Alive2 该插件尝试验证 LLVM 执行的每个 IR 级别转换。像这样调用插件： ``` clang -O3 ~/llvm/clang/test/C/C99/n505.c -S -emit-llvm \ -fpass-plugin=~/alive2/build/tv/tv.so \ -Xclang -load -Xclang ~/alive2/build/tv/tv.so ``` 或者，更方便地： ``` ~/alive2/build/alivecc -O3 -c ~/llvm/clang/test/C/C99/n505.c ~/alive2/build/alive++ -O3 -c ~/llvm/clang/test/Analysis/aggrinit-cfg-output.cpp ``` Clang 插件可以选择使用多核。要启用并行转换验证，请向 Clang 添加 `-mllvm -tv-parallel=XXX` 命令行选项，其中 XXX 是 Alive2 支持的两种并行管理器之一。第一种 (XXX=fifo) 使用 alive-jobserver：有关如何使用此程序的详细信息，请通过运行不带任何命令行参数的程序来查阅其帮助输出。第二种并行管理器 (XXX=unrestricted) 根本不限制并行性，而是自由调用 fork()。这主要用于开发者使用；它往往会占用大量 RAM。 使用 `-mllvm -tv-report-dir=dir` 告诉 Alive2 将其输出文件放入特定目录。 Clang 插件的输出可能非常庞大。为了帮助控制这一点，它支持一个减少输出量的选项 (`-mllvm -tv-quiet`)。 我们的目标是让 `alivecc` 和 `alive++` 编译器驱动程序成为 `clang` 和 `clang++` 的直接替换品。因此，例如，它们试图检测何时被调用为汇编器或链接器，在这种情况下，它们不会加载 Alive2 插件。这意味着如果您手动指定 Alive2 的命令行选项，例如使用 `-DCMAKE_C_FLAGS=...`，则某些项目无法构建。相反，您可以使用通常镜像插件命令行界面的一组环境变量来告诉 `alivecc` 和 `alive++` 做什么。例如： ``` ALIVECC_PARALLEL_UNRESTRICTED=1 ALIVECC_PARALLEL_FIFO=1 ALIVECC_DISABLE_UNDEF_INPUT=1 ALIVECC_DISABLE_POISON_INPUT=1 ALIVECC_SMT_TO=timeout in milliseconds ALIVECC_SUBPROCESS_TIMEOUT=timeout in seconds ALIVECC_OVERWRITE_REPORTS=1 ALIVECC_REPORT_DIR=dir ``` 如果验证程序需要很长时间，您可以批量验证优化。 请设置 `ALIVECC_BATCH_OPTS=1` 并运行 `alivecc`/`alive++`。 ## 运行独立转换验证工具 此工具有两种模式。 在第一种模式下，指定源（原始）和目标（优化后）IR 文件，或者指定包含名为 “src” 的函数和名为 “tgt” 的函数的单个文件。例如，让我们证明删除加法的 `nsw` 是正确的： ``` ~/alive2/build/alive-tv src.ll tgt.ll ---------------------------------------- define i32 @f(i32 %a, i32 %b) { %add = add nsw i32 %b, %a ret i32 %add } => define i32 @f(i32 %a, i32 %b) { %add = add i32 %b, %a ret i32 %add } Transformation seems to be correct! ``` 翻转输入会产生一个反例，因为添加 `nsw` 通常是不正确的。 如果您对使用 `undef` 的反例不感兴趣，可以使用命令行参数 `-disable-undef-input`。 在第二种模式下，指定一个未优化的 IR 文件。alive-tv 将使用类似于 -O2 的优化管道对其进行优化，但没有任何过程间 pass，然后尝试验证转换。 例如，截至 2020 年 2 月 6 日，`release/10.x` 分支包含一个可以按如下方式触发的优化器错误： ``` cat foo.ll define i3 @foo(i3) { %x1 = sub i3 0, %0 %x2 = icmp ne i3 %0, 0 %x3 = zext i1 %x2 to i3 %x4 = lshr i3 %x1, %x3 %x5 = lshr i3 %x4, %x3 ret i3 %x5 } ~/alive2/build/alive-tv foo.ll ---------------------------------------- define i3 @foo(i3 %0) { %x1 = sub i3 0, %0 %x2 = icmp ne i3 %0, 0 %x3 = zext i1 %x2 to i3 %x4 = lshr i3 %x1, %x3 %x5 = lshr i3 %x4, %x3 ret i3 %x5 } => define i3 @foo(i3 %0) { %x1 = sub i3 0, %0 ret i3 %x1 } Transformation doesn't verify! ERROR: Value mismatch Example: i3 %0 = #x5 (5, -3) Source: i3 %x1 = #x3 (3) i1 %x2 = #x1 (1) i3 %x3 = #x1 (1) i3 %x4 = #x1 (1) i3 %x5 = #x0 (0) Target: i3 %x1 = #x3 (3) Source value: #x0 (0) Target value: #x3 (3) Summary: 0 correct transformations 1 incorrect transformations 0 errors ``` 请记住，您不必为了尝试 alive-tv 而编译 Alive2；它可在线获取：https://alive2.llvm.org/ce/ ## 运行独立 LLVM 执行工具 此工具将 Alive2 用作 LLVM 函数的解释器。目前它高度实验性且有许多限制。例如，函数不能接受输入，不能使用内存，不能依赖于未定义行为，并且不能包含执行过多迭代的循环。 ## 缓存 alive-tv 工具和 Alive2 转换验证 opt 插件支持使用外部 Redis 服务器来避免执行冗余查询。此功能并非旨在供一般使用，而是为了加速某些执行大量重复工作的系统性测试工作负载。当它遇到重复的改进检查时，它会打印“Skipping repeated query”而不是执行查询。 如果要使用此功能，则需要根据情况在 localhost 上手动启动和停止 Redis 服务器实例。Alive2 应该是此服务器的唯一用户。 ## 诊断不健全报告 * 选择一个失败的测试文件。选择在包含文本 “(unsound)” 的日志文件开头给出的路径可能很方便；这保证包含不健全报告。然而，许多日志文件仅包含 “Source: \” 而不是文件路径；这些文件的名称以 “in_” 开头。 * 仅针对该文件执行详细运行的 Lit，并附加 `opt` 选项 `--print-after-all`。（您也可以附加其他 `opt` 选项，例如其他优化。）例如： ``` ~/llvm/build/bin/llvm-lit -vva "-Dopt=~/alive2/build/opt-alive.sh --print-after-all" ~/llvm/llvm/test/Transforms/InstCombine/insert-const-shuf.ll ``` * 收集 Lit 的 LLVM IR 终端输出，以便与日志文件中 “Report written to…” 指示的 Alive2 的 Alive2 IR 输出进行比较。有时 Lit 输出可能不包含有用的 LLVM IR，在这种情况下，单独执行输出 RUN 命令可能会给出更好的结果。 * 相应日志文件中的 Alive2 不健全报告将有两个版本的错误优化函数。Alive2 IR 函数体可能会向人类指出问题，但对于 Alive2 转换验证，您需要 LLVM IR。在终端输出中搜索函数名称。 * 将第一个函数定义和必要的声明及元数据复制到新文件或 Alive2 Compiler Explorer 实例，[https://alive2.llvm.org/ce/](https://alive2.llvm.org/ce/)。（`-allow-incomplete-ir` 标志可能会使复制声明和元数据变得不必要。） Alive2 Compiler Explorer 实例将自动运行；要使用独立的 `alive-tv` 进行检查，请参阅其上方的说明。 如果没有第二个版本的函数可供比较，Alive2 只会运行 `-O2` 优化；如果它报告不健全，则您的分支的优化不应受到指责。 * 如果 LLVM IR 终端输出中有第二个不健全的函数定义，请复制它和必要的声明，并更改第二个函数名称。 * 如果它现在报告错误优化，据推测您的分支有一个错误，由提供的示例演示。 * 要在比较不同的测试运行时筛选出完全重复的报告，请在每次运行之前将 `logs` 目录移开。每次运行后，将相关日志复制到单独的目标目录。（具有非 GNU 版本 `cp` 的系统需要使用 coreutils 的 `gcp`。） ``` fgrep --files-with-matches --recursive "(unsound)" ~/alive2/build/logs/ | xargs cp -p --target-directory= ``` * 然后可以使用诸如 `jdupes --print-unique` 之类的实用程序找到唯一的不健全报告。 * 如果测试是在不同的 LLVM 目录上运行的，则在比较之前应去除名称不以 “in_” 开头的文件中的 “Source:” 行，以及 Linux 上的 “Command line:” 行。 ## 故障排除 * 如果遇到构建问题，请检查 CMake 输出的 “LLVMConfig.cmake” 和 “CMAKE_PREFIX_PATH”。如果这些设置不正确，CMake 可能会在 LLVM 的旧安装位置（例如 `/opt/` 下）查找配置信息。 * 某些 Clang 和 MacOS 版本的组合可能会给出链接警告 “-undefined dynamic_lookup may not work with chained fixups,” 以及带有 “symbol not found in flat namespace.” 的运行时错误。在 CMakeLists.txt 的开头将 [CMAKE_OSX_DEPLOYMENT_TARGET](https://cmake.org/cmake/help/latest/variable/CMAKE_OSX_DEPLOYMENT_TARGET.html) 设置为 11.0 或更小的缓存条目可能会解决此问题。 * 转换验证的构建与 LLVM 源码树顶部紧密耦合。使用较旧源码构建分支可能需要恢复到相应的 Alive2 提交。这反过来可能需要对 Clang 和 SDK 版本及供应商进行试验。 * 在最新的机器上构建较旧的源码可能需要调整。例如，现已删除的文件 `scripts/rewritepass.py` 依赖于已弃用的 Python 2；将 shebang 行更新为 `python3`。 * `opt` 包装脚本 `build/opt-alive.sh` 接受一个 `--verbose` 选项，该选项输出传递给 `opt` 的命令。请注意，这可能会干扰检查输出的测试。 * 该脚本还接受一个 `--no-timeout` 选项，该选项禁用 `opt` 进程超时。Macintosh 不支持此超时。要更改 SMT 超时，请改为向 `alive` 可执行文件传递 `-smt-to:` 选项。 ## Alive2 发现的 LLVM 错误 [BugList.md](BugList.md) 显示了 Alive2 发现的 LLVM 错误列表。

标签：Alive2, Bash脚本, C++, Clang, LLVM, SMT求解器, UB检测, Z3, 中间代码, 云安全监控, 代码优化验证, 可配置连接, 形式化验证, 数据擦除, 程序分析, 符号执行, 编译器, 编译器安全, 编译器验证, 翻译验证, 静态分析