CoBRA 混合布尔-算术表达式化简器

使用条件与局限

• 审阅时最新版本为 v1.3.0，发布于 2026-06-30，未附带预编译二进制。所审阅的 master 提交比该版本多八个提交：修改 README、升级 CI 依赖、改为仅在构建优化遍插件时才要求 LLVM，以及使 cobra-core 能用 MSVC 构建。本条目固定该提交仅用于引用文档。
• 从源码构建需要 CMake 3.20+ 和 C++23 编译器（GCC 13+、Clang 17+ 或 Apple Clang 16+）；依赖超级构建会编译 Abseil 和 Highway，启用测试时还会编译 GoogleTest。LLVM 优化遍插件需要 LLVM 19 至 22，通过 opt 以 cobra-simplify 名称运行，仅在化简结果开销更低时才替换表达式，并会丢弃 nuw/nsw 标志。只有 CMake 找到 Z3 时才会编译 Z3 校验功能，否则 cobra-cli 会提示 --verify 被忽略。CI 每次都在 Ubuntu 24.04 上用 Clang 22 和 LLVM 22 构建，GCC 14 和 macOS 15 构建仅针对版本标签运行；Windows 不在 CI 范围内。
• cobra-cli 以文本形式接收混淆表达式，默认最多 16 个变量，因此二进制中的表达式须先借助其他工具恢复，或以 LLVM IR 形式交给优化遍处理。README 列出的已知局限包括：算术与按位运算深度交织、提升后仍耗尽工作列表预算的混合多项式 MBA；少数只在布尔输入上成立、因而被报告为校验失败的候选结果；以及不提供通用逻辑最小化。
• README 报告共有 1,195 项测试；DATASETS.md 报告，在来自七个来源、35 个数据集文件的 75,126 个可解析表达式中，有 75,023 个完成化简并通过抽查（99.86%）。OSES 子集因内存耗尽或每个表达式需耗时数分钟而被停用，其数字来自此前的一次运行；DATASETS.md 称这些数字在每次 CI 运行时都会核对，但所审阅的 CI 工作流排除了数据集基准测试。
• CoBRA 本身采用 Apache-2.0 许可。test/datasets 中的文件转载自第三方研究项目：THIRD_PARTY_LICENSES 将其中大部分列为实际适用 GPL-3.0-only，Loki 数据集为 AGPL-3.0-only，OSES 和 ObfuscatorX 数据集的许可证未说明或未知。本次未构建或运行任何内容。

关于此条目

说明已依据一手来源复核；这不代表已运行验证、经过安全审计或确认兼容。

报告条目过时 ↗建议修正翻译 ↗

一手来源

1. README.md GitHub · trailofbits/CoBRA · 修订 af44b8a
2. BUILD.md GitHub · trailofbits/CoBRA · 修订 af44b8a
3. DATASETS.md GitHub · trailofbits/CoBRA · 修订 af44b8a
4. THIRD_PARTY_LICENSES GitHub · trailofbits/CoBRA · 修订 af44b8a
5. docs/methodology/README.md GitHub · trailofbits/CoBRA · 修订 af44b8a
6. CMakeLists.txt GitHub · trailofbits/CoBRA · 修订 af44b8a
7. tools/cobra-cli/main.cpp GitHub · trailofbits/CoBRA · 修订 af44b8a
8. lib/llvm/CobraPass.cpp GitHub · trailofbits/CoBRA · 修订 af44b8a
9. test/llvm/CMakeLists.txt GitHub · trailofbits/CoBRA · 修订 af44b8a
10. .github/workflows/ci.yml GitHub · trailofbits/CoBRA · 修订 af44b8a
11. LICENSE GitHub · trailofbits/CoBRA · 修订 af44b8a
12. https://github.com/trailofbits/CoBRA/releases/tag/v1.3.0