0.如题

我使用的是verilator和klee进行符号执行的学习，目前还处于起步阶段，起步阶段除了要了解符号执行的定义和作用之外就是环境的搭建了，没想到搭建环境这一步就浪费了很多时间，主要问题出在按照官方的步骤进行搭建的时候，总是各种报错+版本依赖问题，在网上排查的时候，发现要改的内容太多，遂使用docker的方式进行快速搭建，在搭建的时候目前最推荐的是启动klee3的容器，在klee3的容器里安装verilator5.0这个方式是最好的组合，因为安装verilator要比安装klee3不管是虚拟机方式还是docker容器里安装都要顺利的多。

但是问题来了，在 Verilator 的不同版本中，访问 Verilog 模块内部信号的方式有所变化，特别是在 3.9 版本和 4.0 及以上版本之间。

Verilator 3.9 版本：

在此版本中，Verilator 允许用户通过生成的 C++ 模型直接访问模块的内部信号。这意味着，即使信号未被显式标记为公共的，用户仍然可以在 C++ 测试平台中访问这些信号。

Verilator 4.0 及以上版本：

从 4.0 版本开始，Verilator 引入了更严格的访问控制机制。为了在 C++ 测试平台中访问模块的内部信号，用户必须在 Verilog 代码中使用特定的注释标记这些信号为公共的。

这就导致一个问题，Verilator 3.9 允许测试代码直接访问模块内部寄存器如 Drg, Dnext, Knext 等，是进行故障注入和中间状态可观测性验证最方便的版本。而从 Verilator 4.0 起，默认不再暴露这些内部变量，除非在 Verilog 中显式添加 // verilator public 标记，因此本研究选择使用 Verilator 3.9 是为了保留对中间状态的完全可控与可观察能力。

但是klee3里安装verilator3的话版本依赖又冲突了装不上去，主要原因是

系统源和包管理器不再提供 Verilator 3.9

klee3 容器环境是基于Ubuntu22.04，而 Verilator 3.9 是较老的版本：

在 Ubuntu 官方仓库中已经移除了 verilator 3.x 的支持，默认 apt install verilator 安装的是 Verilator 4.02+。

即使尝试手动编译 Verilator 3.9，也会出现 C++ 标准兼容性问题（C++11/14 与新版编译器冲突），例如：

error: ISO C++17 does not allow dynamic exception specifications

KLEE 容器中环境依赖冲突

klee3 容器本身：

使用的是基于 LLVM 13/14 的工具链（通过 /tmp/llvm-130-install_O_D_A 路径可以确认）；

该环境为保证 KLEE 符号执行兼容性，禁用了较多系统服务（如 GUI、动态包拉取等）；

一些老版本 Verilator 依赖的工具（如旧版 Flex/Bison 或 autotools 组件）在 KLEE 容器里版本不兼容或缺失；

make install 阶段缺乏写权限或链接环境变量未配置完整。

基于以上原因，我提出了一种折衷的办法，那就是创建两个容器，一个是klee3一个是verilator3，这两个容器通过共享文件夹的方式对代码进行各司其职的操作，为行文方便，以下统称k3v3。 代码编写完成后放在共享文件夹里，首先使用v3进行模型转换，再使用k3进行符号执行。

1.符号执行

1.1.定义

符号执行是一种程序分析技术，其核心思想是将程序的输入表示为符号变量而非具体值，并沿程序的各条执行路径模拟执行，同时记录路径条件（Path Condition）——即一系列限制符号变量的逻辑约束。最终，符号执行引擎可通过约束求解器（如 Z3）验证路径可达性，或生成触发特定行为的输入。

这种技术广泛应用于自动化测试用例生成、程序验证、安全漏洞检测、逆向分析与加密协议验证等领域。

1.2.分类

符号执行根据执行方式和路径探索策略，可大致分为以下几类：

• 静态符号执行（Pure Symbolic Execution）

以完全符号化输入执行程序，探索所有可能路径。

优点：理论完备，能覆盖所有逻辑路径。

缺点：易受路径爆炸影响，对环境建模要求高。

• 动态符号执行（Concolic Execution，Concrete + Symbolic）

在真实输入驱动下执行程序，同时进行符号跟踪。

结合符号与具体值，能够更高效发现深层路径。

代表工具：KLEE、SAGE、Angr（支持二进制级 concolic 执行）。

• 路径敏感符号执行（Path-sensitive SE）

精细分析每条路径上的约束条件，避免路径合并。

优点：精准，适合断言验证与精确漏洞定位。

缺点：路径数目呈指数增长，需剪枝与缓存策略。

• 符号执行与模糊测试混合

将符号执行与 AFL/Fuzz 等模糊测试相结合，用符号执行补齐模糊测试难以覆盖的路径。

代表系统：Driller、QSYM、Hybrid-Fuzz。

2.verilator+klee

2.1.verilator

Verilator 是一种开源的 Verilog/SystemVerilog 到 C++/SystemC 的转换工具，它被广泛用于高性能仿真和验证数字硬件设计。

Verilator 会将 Verilog 或 SystemVerilog 代码转换（“Verilate”）成等效的 C++ 或 SystemC 模型代码。这些模型可以通过通用 C++ 编译器（如 gcc、clang）进行编译，然后运行以完成硬件电路的仿真。

Verilator 的主要功能：

静态转换： Verilator 不会解释运行时行为，而是将设计静态地转换为 C++ 代码，这使得仿真速度远高于传统解释型仿真器。

代码检查： 自动执行 Lint（语法和风格）检查，识别潜在问题。

断言与覆盖率支持： 可选插入断言检查点与覆盖率分析点，用于验证设计正确性。

多线程支持： 可生成多线程 C++ 模型，提高大规模设计的仿真效率。

高性能： 适合对复杂芯片级设计进行百万次周期级别的快速仿真。

与其他工具集成： 支持将 Verilated 代码封装成库，可与其他仿真器或工具链（如 SystemC、KLEE）集成。

Verilator 不适合的场景：

不能处理 SDF 注释（时序信息注入）；

不支持混合信号仿真（模拟+数字）；

不推荐用于快速课程作业（推荐使用 Icarus Verilog）；

不具备 GUI 波形工具（但可输出 VCD 波形与 GTKWave 配合）。

使用 Verilator 的典型场景：

在芯片设计流程中替代传统慢速仿真器；

结合 KLEE 等符号执行工具进行硬件验证；

将 RTL 设计嵌入到 C++ 模拟环境或测试平台；

将硬件 IP 转为 C++，嵌入 AI 模型或软件控制流程中。

2.2.klee

KLEE 是一个基于 LLVM 的开源符号执行工具，用于自动生成高覆盖率测试用例，并发现程序中的潜在缺陷。它特别适合分析 C/C++ 语言编写的系统程序、加密算法实现和嵌入式软件，在学术界和工业界均有广泛应用。

KLEE 的核心机制是将程序输入视为符号变量，在执行程序时记录路径条件，并通过约束求解器生成覆盖各执行路径的具体输入。该过程无需预先指定输入集合，即可自动探索程序中的分支、错误路径和安全边界。

KLEE 的主要功能：

符号执行引擎： 支持执行 LLVM 位码程序，自动构造路径约束条件；

自动化测试用例生成： 输出能覆盖不同分支路径的具体输入，用于验证程序行为；

错误检测与断言验证： 自动捕捉如内存溢出、除零、断言失败等运行时错误；

POSIX 模拟层： 模拟系统调用、文件 I/O、环境变量等运行环境，提升现实适配度；

路径探索策略： 支持 DFS、BFS、随机路径等搜索算法，用于控制状态空间爆炸；

输入重放与分析： 支持将生成的 .ktest 文件回放到原生环境中进行调试与验证。

KLEE 的局限与注意事项：

不直接支持完整的 C++ STL 和多线程；

执行效率受限于路径爆炸与约束求解器性能；

需配合 LLVM 工具链使用，预处理阶段对构建环境要求较高；

某些外部库或系统调用需模拟或封装支持。

KLEE 的典型应用场景：

软件安全性验证： 检测加密算法中的差错传播、密钥恢复条件等安全属性；

自动化单元测试生成： 提高测试覆盖率，发现边界条件缺陷；

嵌入式系统验证： 配合 Verilator 分析 Verilog 转 C++ 的硬件模型行为；

漏洞挖掘与 CTF 工具链： 在安全研究中用于符号路径约束分析和自动反例生成。

3.环境搭建

3.1.创建虚拟机共享文件夹

mkdir /home/hx/hxv3k3
cp file /home/hx/hxv3k3
chmod 777 /home/hx/hxv3k3

3.2.verilator

sudo docker run -itd --name veri3 
  --entrypoint /bin/bash 
  -v /home/hx/hxv3k3:/home/hxh   
  13816a918f61 -c "tail -f /dev/null"
  
  sudo docker exec -it veri3 /bin/bash

3.3.klee

sudo docker run -itd --name veri3 -v /home/hx/hxv3k3:/home/hxh 13816a918f61 tail -f /dev/null
sudo docker exec -it klee3 /bin/bash 

4.环境运行方式

4.1.verilator

/aes_config.sh
TOP_MODULE="AES_ENC"
CORE_DIR="/home/hxh/aes/1aes/cores"
TESTBENCH="tb_AES_CF.cpp"
EXE_DIR="/home/hxh/aes/1aes/exe"
VERILATOR_OUT="$EXE_DIR/verilator_out"
VERILATOR_INCLUDE="/home/hxh/verilator_include"
VERILATOR_BIN="/home/hxh/verilator_bin"

/build_verilator3.sh
#!/bin/bash
set -e
source /home/hxh/aes_config.sh

step() { echo -e "n33[1;36m🔷 Step $1: $233[0m"; sleep 0.4; }
run() { echo -e "   33[90m$@33[0m"; sleep 0.2; eval "$@"; }

step 1 "准备工作目录"
run "cd $EXE_DIR"
[ -d "$VERILATOR_OUT" ] && echo "⚠️ $VERILATOR_OUT 已存在，跳过清理" || run "mkdir -p $VERILATOR_OUT"

step 2 "生成 Verilator C++ 模块"
run "verilator -O3 -Wall -language 1364-2001 --top-module $TOP_MODULE 
  -Wno-UNOPTFLAT +incdir+$CORE_DIR 
  -Mdir $VERILATOR_OUT -cc $CORE_DIR/*.v --exe $TESTBENCH"

step 3 "拷贝 include 和 bin 到共享目录"
[ -d "$VERILATOR_INCLUDE" ] || run "cp -r /usr/local/share/verilator/include $VERILATOR_INCLUDE"
[ -d "$VERILATOR_BIN" ] || run "cp -r /usr/local/share/verilator/bin $VERILATOR_BIN"

echo -e "n33[1;32m✅ Verilator 构建完成：$VERILATOR_OUT33[0m"

4.2.klee

#!/bin/bash
set -e

step() {
    echo -e "n33[1;36m🔷 Step $1: $233[0m"
    sleep 0.5
}

run() {
    echo -e "   33[90m$@33[0m"
    sleep 0.2
    eval "$@"
}

step "1" "挂载头文件与工具链"
run "sudo mkdir -p /usr/local/share/verilator"
run "sudo ln -sf /home/hxh/verilator_include /usr/local/share/verilator/include"
run "sudo ln -sf /home/hxh/verilator_bin /usr/local/share/verilator/bin"

step "2" "拷贝所有生成文件到工作目录 /tmp/aes_test"
run "rm -rf /tmp/aes_test"
run "mkdir -p /tmp/aes_test"
cd /tmp/aes_test
run "cp /home/hxh/aes/1aes/exe/tb_AES_CF.cpp ."
run "cp /home/hxh/aes/1aes/exe/verilator_out/*.cpp ."
run "cp /home/hxh/aes/1aes/exe/verilator_out/*.h ."
run "cp /home/hxh/verilator_include/verilated.cpp ."

step "3" "建立 obj_dir 链接（用于模拟 verilated 路径）"
run "mkdir -p obj_dir"
run "ln -sf ../VAES_ENC.h obj_dir/VAES_ENC.h"
run "ln -sf ../VAES_ENC__Syms.h obj_dir/VAES_ENC__Syms.h"

step "4" "使用 wllvm++ 编译为 .o 文件（带调试信息）"
export LLVM_COMPILER=clang
run "wllvm++ -g -c tb_AES_CF.cpp -I. -I/usr/local/share/verilator/include -I/usr/local/share/verilator/include/vltstd"
run "wllvm++ -g -c VAES_ENC.cpp -I. -I/usr/local/share/verilator/include -I/usr/local/share/verilator/include/vltstd"
run "wllvm++ -g -c VAES_ENC__Syms.cpp -I. -I/usr/local/share/verilator/include -I/usr/local/share/verilator/include/vltstd"
run "wllvm++ -g -c verilated.cpp -I/home/hxh/verilator_include -I/home/hxh/verilator_include/vltstd"

step "5" "提取 .bc 文件（extract-bc）"
run "extract-bc tb_AES_CF.o"
run "extract-bc VAES_ENC.o"
run "extract-bc VAES_ENC__Syms.o"
run "extract-bc verilated.o"

step "6" "合并为 VAES_ENC.bc（llvm-link）"
run "llvm-link tb_AES_CF.o.bc VAES_ENC.o.bc VAES_ENC__Syms.o.bc verilated.o.bc -o VAES_ENC.bc"

step "7" "运行 KLEE（基础执行）"
run "klee --libc=uclibc --search=dfs --output-dir=klee-out-basic VAES_ENC.bc"

step "8" "运行 KLEE（输出路径与全部错误）"
run "klee --libc=uclibc --emit-all-errors --write-paths --search=dfs --output-dir=klee-out-full VAES_ENC.bc"

step "9" "运行 KLEE（生成路径执行图）"
run "klee --libc=uclibc --emit-all-errors --write-paths --write-exec-tree --search=dfs --output-dir=klee-out-tree VAES_ENC.bc"
run "klee-exec-tree tree-dot klee-out-tree | dot -Tsvg > tree.svg"

step "10" "将 tree.svg 导出到宿主机目录"
run "cp /tmp/aes_test/tree.svg /home/hxh/"
echo -e "n33[1;32m✅ SVG 路径图已导出至宿主机：/home/hxh/tree.svg33[0m"

5.运行效果截图

正如前文所说，本人还在初学阶段，所以写的代码并不符合符号执行的条件，所以就不放代码了，放一段运行成功的截图。