stp/stp

[](https://opensource.org/licenses/MIT) [](https://ci.appveyor.com/project/msoos/stp) [](https://stp.readthedocs.io/en/latest/?badge=latest) [](https://scan.coverity.com/projects/861) # STP STP 是一个约束求解器（或 SMT 求解器），旨在解决位向量和数组的约束问题。这些类型的约束可以由程序分析工具、定理证明器、自动错误查找器、密码攻击工具、智能模糊测试器、模型检查器以及许多其他应用程序生成。 * 主页： https://stp.github.io/ * Ubuntu PPA： https://launchpad.net/~simple-theorem-prover/+archive/ubuntu/ppa/+packages * Docker 镜像： `docker pull msoos/stp` ## 构建和安装 快速安装： ``` sudo apt-get install git cmake bison flex libboost-all-dev libgmp-dev python2 perl git clone https://github.com/stp/stp cd stp git submodule init && git submodule update ./scripts/deps/setup-gtest.sh ./scripts/deps/setup-outputcheck.sh ./scripts/deps/setup-cms.sh ./scripts/deps/setup-minisat.sh mkdir build cd build cmake .. cmake --build . sudo cmake --install . ``` 或者，使用 [Homebrew](https://brew.sh)： ``` brew install stp ``` 有关更详细的说明，请参阅页面末尾。 ## 输入格式 [SMT-LIB2](https://smtlib.cs.uiowa.edu/language.shtml) 格式是推荐的文件格式，因为所有现代位向量求解器都可以解析它。在 SMT-LIB2 格式中，仅实现了无量词位向量和数组。 ### 用法 使用 SMT-LIB2 文件运行： ``` stp myproblem.smt2 ``` 使用 Python 接口溢出 32 位整数： ``` import stp In [1]: import stp In [2]: a = stp.Solver() In [3]: x = a.bitvec('x') In [4]: y = a.bitvec('y') In [5]: a.add(x + y < 20) In [6]: a.add(x > 10) In [7]: a.add(y > 10) In [8]: a.check() Out[8]: True In [9]: a.model() Out[9]: {'x': 4294967287L, 'y': 11L} ``` 使用 Docker： ``` docker pull msoos/stp echo "(set-logic QF_BV) (assert (= (bvsdiv (_ bv3 2) (_ bv2 2)) (_ bv0 2))) (check-sat) (exit)" | docker run --rm -i msoos/stp ``` ## 架构 系统执行字级预处理，随后转换为 SAT，然后由 SAT 求解器进行求解。特别是，我们在预处理步骤中引入了几种新的启发式方法，包括数组上下文中的抽象-细化、一种新的位向量线性算术方程求解器，以及一些有趣的简化。这些启发式方法帮助我们在性能上比其他工具以及直接转换为 SAT 实现了几个数量级的提升。STP 已经在源自各种实际应用（如程序分析和错误查找工具 EXE，以及等价性检查工具和定理证明器）的数千个示例上进行了严格测试。 ## 详细的构建和安装 STP 使用 [CMake](https://cmake.org/) 3.0.2 或更高版本进行构建。CMake 是一个 元构建系统，可为其他工具（如 make(1)、Visual Studio、Xcode 等）生成构建文件。 ### 配置变量 以下是一些有用的配置变量。这些适用于所有 生成器。 - `CMAKE_BUILD_TYPE` - 构建类型（例如 Release） - `CMAKE_INSTALL_PREFIX` - 安装的前缀（例如 /usr/local ） - `ENABLE_ASSERTIONS` - 如果为 TRUE，STP 将在构建时包含断言。 - `ENABLE_TESTING` - 启用测试运行 - `ENABLE_PYTHON_INTERFACE` - 启用 Python 接口的构建 - `PYTHON_EXECUTABLE` - 如果安装了多个 python，请设置 python 可执行文件 - `SANITIZE` - 使用 Clang 的消毒器检查 - `STATICCOMPILE` - 构建静态库和二进制文件而不是动态文件 ### 依赖项 STP 依赖于：boost、flex、bison 和 minisat。您可以通过以下方式安装它们： ``` $ sudo apt-get install cmake bison flex libboost-all-dev python perl minisat ``` 如果您的发行版没有附带 minisat，STP 维护了一个更新的分支。可以按如下方式构建： ``` $ git clone https://github.com/stp/minisat $ cd minisat $ mkdir build && cd build $ cmake .. $ cmake --build . $ sudo cmake --install . $ command -v ldconfig && sudo ldconfig ``` STP 默认使用 minisat 作为其 SAT 求解器，但它也支持其他 SAT 求解器，包括作为可选附加组件的 CryptoMiniSat。如果已安装，将在 cmake 期间检测到并使用它： ``` $ git clone https://github.com/msoos/cryptominisat $ cd cryptominisat $ mkdir build && cd build $ cmake .. $ cmake --build . $ sudo cmake --install . $ command -v ldconfig && sudo ldconfig ``` 或者，这些命令已在 `scripts/deps/setup-minisat.sh` 和 `scripts/deps/setup-cms.sh` 中预配置（分别为两者）。 #### 针对未安装的库进行构建 如果您希望在不安装 STP 依赖项的情况下构建它们，您可以告诉 CMake 在哪里可以找到这些未安装的文件。例如： * `-DMINISAT_INCLUDE_DIRS:PATH=` 和 `-DMINISAT_LIBDIR:PATH=` -- 分别为 `minisat/core/Solver.h` 和 `minisat` 库的路径 * `-Dcryptominisat5_DIR:PATH=` -- `cryptominisat5Config.cmake` 的路径 如果您没有安装这些开发库，则可以将 `MINISAT_LIBDIR` 设置为您的 minisat `build` 文件夹，并将 `cryptominisat5_DIR` 设置为您的 CryptoMiniSat 的 `build` 文件夹。 ### 构建静态库和二进制文件 ``` $ mkdir build && cd build $ cmake -DSTATICCOMPILE=ON .. $ cmake --build . $ sudo cmake --install . $ command -v ldconfig && sudo ldconfig ``` ### 配置和构建选项 要调整构建配置： * 运行 `cmake-gui /path/to/stp/source/root` 而不是 `cmake`。这个 用户界面允许您控制各种配置 变量的值，并让您选择构建系统生成器。 * 运行 `ccmake` 而不是 `cmake`。这提供了一个 ncurses 终端 界面来更改配置变量。 * 将 `-D=` 选项传递给 `cmake`（用户体验不佳）。 如果您正在编写 脚本，那么**仅**以这种方式配置可能是最好的。 您也可以稍后通过运行 `make edit_cache` 调整配置，编辑任何配置变量，重新配置，然后重新生成构建系统。配置完成后，通过运行 `make` 进行构建。 您可以使用 `-j` 标志通过并行运行 `` 个作业来显著减少构建时间（例如，`make -j4`）。 ### 测试 ``` git clone https://github.com/stp/stp git submodule update --init pip install lit mkdir build cd build cmake -DENABLE_TESTING=ON .. make make test ``` ### 安装 要安装，请运行 `make install`；要卸载，请运行 `make uninstall`。安装的根目录由配置时的 `CMAKE_INSTALL_PREFIX` 变量控制。您可以通过运行 `make edit_cache` 并编辑 `CMAKE_INSTALL_PREFIX` 的值来更改此设置。 ### 在 Windows/Visual Studio 上构建 您需要安装 [cmake](https://cmake.org/download/) 并按照 AppVeyor [遵循](https://github.com/stp/stp/blob/master/appveyor.yml) 的步骤进行操作。如果您需要静态二进制文件，您始终可以在 [AppVeyor 构建页面](https://ci.appveyor.com/project/msoos/stp) 上将其作为构建产物获取。如果您仍然遇到问题，请查看 [在 issue #319 中](https://github.com/stp/stp/issues/319) 的微型 HOWTO。 ### 构建 Docker ``` git clone https://github.com/stp/stp cd stp docker build -t stp . echo "(set-logic QF_BV) (assert (= (bvsdiv (_ bv3 2) (_ bv2 2)) (_ bv0 2))) (check-sat) (exit)" | docker run --rm -i stp ``` # 作者 * Vijay Ganesh * Trevor Hansen * Mate Soos * Dan Liew * Ryan Govostes * Andrew V. Jones * 以及许多其他人...

标签：Bash脚本, SMT求解器, 位向量, 可配置连接, 定理证明器, 形式化验证, 程序分析, 约束求解, 请求拦截, 逆向工具