我是 SMT 求解器和这些主题的新手。我需要将 C++ 代码转换为 SMT2 的等效代码（我有一个需要 .smt2 作为输入的工具）。我已经找到了这个解决方案，但它没有完全解释如何做到这一点？你能帮我一下吗？谢谢
while (x<y)
{
x=5*x+3;
y=3*y+5;
w=3*z+w;
z=z+6;
}
有没有什么工具可以进行这种转换？或者我应该如何了解这个主题？
如果您正在寻找一个可以将任意 C++ 转换为 SMTLib 的工具，那么我认为这样的工具不存在，也不可行，因为这意味着您需要非常精确的 C++ 语义在 SMTLib 中编码，即使不是不可能，也是一项艰巨的任务。
如果您关心有限的子集，或者只想手动翻译一两个具体示例，那么您找到的答案就很好。首先研究SMTLib本身，并查找SSA（单一静态分配）。循环会很困难，但有一些方法可以处理它们。同样，这完全取决于您到底想要实现什么目标。一旦您查看了这些选项，也许您可以提出更具体的问题。
这样做也不可行
这是可行的。 CBMC 可以做到。有点烦人的是，对于未“使用”的功能，它不会输出 SMT2。考虑这个程序：
int foo(int x, int y) {
int w = 0;
int z = 0;
// while (x<y) {
x = 5*x+3;
y = 3*y+5;
w = 3*z+w;
z = z+6;
// }
return z;
}
int main() {
int x;
int y;
assert(foo(x, y) == 4);
}
您可以这样验证：
❯ cbmc foo.c
CBMC version 5.11 (cbmc-5.11) 64-bit x86_64 linux
...
Solving with MiniSAT 2.2.1 with simplifier
850 variables, 2775 clauses
SAT checker: instance is SATISFIABLE
Runtime decision procedure: 0.00147982s
** Results:
foo.c function main
[main.assertion.1] line 16 assertion return_value_foo == 4: FAILURE
** 1 of 1 failed (1 iteration)
VERIFICATION FAILED
你可以像这样告诉它生成smt2：
❯ cbmc --smt2 foo.c --function foo --outfile foo.smt2
CBMC version 5.11 (cbmc-5.11) 64-bit x86_64 linux
Parsing foo.c
Converting
Type-checking foo
file foo.c line 16 function main: function `assert' is not declared
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
size of program expression: 46 steps
simple slicing removed 0 assignments
Generated 0 VCC(s), 0 remaining after simplification
VERIFICATION SUCCESSFUL
但是，如果您检查该文件，它是空的：
❯ cat foo.smt2
; SMT 2
(set-info :source "Generated by CBMC 5.11 (cbmc-5.11)")
(set-option :produce-models true)
(set-logic QF_AUFBV)
那是因为我们告诉它只验证
foomain❯ cbmc --smt2 foo.c --outfile foo.smt2
CBMC version 5.11 (cbmc-5.11) 64-bit x86_64 linux
Parsing foo.c
Converting
Type-checking foo
file foo.c line 16 function main: function `assert' is not declared
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
size of program expression: 49 steps
simple slicing removed 5 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to SMT2
converting SSA
Running SMT2
Runtime decision procedure: 0.000140233s
❯ cat foo.smt2
; SMT 2
(set-info :source "Generated by CBMC 5.11 (cbmc-5.11)")
(set-option :produce-models true)
(set-logic QF_AUFBV)
; set_to true (equal)
(define-fun |__CPROVER_dead_object#1| () (_ BitVec 64) (_ bv0 64))
; set_to true (equal)
(define-fun |__CPROVER_deallocated#1| () (_ BitVec 64) (_ bv0 64))
; set_to true (equal)
(define-fun |__CPROVER_malloc_is_new_array#1| () Bool false)
; set_to true (equal)
(define-fun |__CPROVER_malloc_object#1| () (_ BitVec 64) (_ bv0 64))
; set_to true (equal)
(define-fun |__CPROVER_malloc_size#1| () (_ BitVec 64) (_ bv0 64))
; set_to true (equal)
(define-fun |__CPROVER_memory_leak#1| () (_ BitVec 64) (_ bv0 64))
; set_to true (equal)
(define-fun |__CPROVER_next_thread_id#1| () (_ BitVec 64) (_ bv0 64))
; set_to true (equal)
(define-fun |__CPROVER_pipe_count#1| () (_ BitVec 32) (_ bv0 32))
; set_to true (equal)
(define-fun |__CPROVER_rounding_mode!0#1| () (_ BitVec 32) (_ bv0 32))
; set_to true (equal)
(define-fun |__CPROVER_thread_id!0#1| () (_ BitVec 64) (_ bv0 64))
; the following is a substitute for lambda i. x
(declare-fun array_of.0 () (Array (_ BitVec 64) (_ BitVec 1)))
; set_to true (equal)
(define-fun |__CPROVER_threads_exited#1| () (Array (_ BitVec 64) (_ BitVec 1)) array_of.0)
; find_symbols
(declare-fun |main::1::x!0@1#1| () (_ BitVec 32))
; set_to true (equal)
(define-fun |foo::x!0@1#1| () (_ BitVec 32) |main::1::x!0@1#1|)
; find_symbols
(declare-fun |main::1::y!0@1#1| () (_ BitVec 32))
; set_to true (equal)
(define-fun |foo::y!0@1#1| () (_ BitVec 32) |main::1::y!0@1#1|)
; set_to true (equal)
(define-fun |foo::1::w!0@1#2| () (_ BitVec 32) (_ bv0 32))
; set_to true (equal)
(define-fun |foo::1::z!0@1#2| () (_ BitVec 32) (_ bv0 32))
; set_to true (equal)
(define-fun |foo::x!0@1#2| () (_ BitVec 32) (bvadd (bvmul (_ bv5 32) |foo::x!0@1#1|) (_ bv3 32)))
; set_to true (equal)
(define-fun |foo::y!0@1#2| () (_ BitVec 32) (bvadd (bvmul (_ bv3 32) |foo::y!0@1#1|) (_ bv5 32)))
; set_to true (equal)
(define-fun |foo::1::w!0@1#3| () (_ BitVec 32) (_ bv0 32))
; set_to true (equal)
(define-fun |foo::1::z!0@1#3| () (_ BitVec 32) (_ bv6 32))
; set_to true (equal)
(define-fun |foo#return_value!0#1| () (_ BitVec 32) (_ bv6 32))
; set_to true (equal)
(define-fun |main::$tmp::return_value_foo!0@1#2| () (_ BitVec 32) (_ bv6 32))
; convert
(define-fun |B0| () Bool (= |main::1::x!0@1#1| |main::1::x!0@1#1|))
; convert
(define-fun |B1| () Bool (= |main::1::y!0@1#1| |main::1::y!0@1#1|))
; find_symbols
(declare-fun |main::$tmp::return_value_foo!0@1#1| () (_ BitVec 32))
; convert
(define-fun |B2| () Bool (= |main::$tmp::return_value_foo!0@1#1| |main::$tmp::return_value_foo!0@1#1|))
; find_symbols
(declare-fun |foo::1::w!0@1#1| () (_ BitVec 32))
; convert
(define-fun |B3| () Bool (= |foo::1::w!0@1#1| |foo::1::w!0@1#1|))
; find_symbols
(declare-fun |foo::1::z!0@1#1| () (_ BitVec 32))
; convert
(define-fun |B4| () Bool (= |foo::1::z!0@1#1| |foo::1::z!0@1#1|))
; set_to false
(assert (not false))
; find_symbols
(declare-fun |symex::args::0| () (_ BitVec 32))
; set_to true
(assert (= |main::1::x!0@1#1| |symex::args::0|))
; find_symbols
(declare-fun |symex::args::1| () (_ BitVec 32))
; set_to true
(assert (= |main::1::y!0@1#1| |symex::args::1|))
(check-sat)
(get-value (|B0|))
(get-value (|B1|))
(get-value (|B2|))
(get-value (|B3|))
(get-value (|B4|))
(get-value (|__CPROVER_dead_object#1|))
(get-value (|__CPROVER_deallocated#1|))
(get-value (|__CPROVER_malloc_is_new_array#1|))
(get-value (|__CPROVER_malloc_object#1|))
(get-value (|__CPROVER_malloc_size#1|))
(get-value (|__CPROVER_memory_leak#1|))
(get-value (|__CPROVER_next_thread_id#1|))
(get-value (|__CPROVER_pipe_count#1|))
(get-value (|__CPROVER_rounding_mode!0#1|))
(get-value (|__CPROVER_thread_id!0#1|))
(get-value (|__CPROVER_threads_exited#1|))
(get-value (|foo#return_value!0#1|))
(get-value (|foo::1::w!0@1#1|))
(get-value (|foo::1::w!0@1#2|))
(get-value (|foo::1::w!0@1#3|))
(get-value (|foo::1::z!0@1#1|))
(get-value (|foo::1::z!0@1#2|))
(get-value (|foo::1::z!0@1#3|))
(get-value (|foo::x!0@1#1|))
(get-value (|foo::x!0@1#2|))
(get-value (|foo::y!0@1#1|))
(get-value (|foo::y!0@1#2|))
(get-value (|main::$tmp::return_value_foo!0@1#1|))
(get-value (|main::$tmp::return_value_foo!0@1#2|))
(get-value (|main::1::x!0@1#1|))
(get-value (|main::1::y!0@1#1|))
(get-value (|symex::args::0|))
(get-value (|symex::args::1|))
(exit)
; end of SMT2 file
希望有帮助。老实说，我还没有真正使用过这个，所以我不知道输出有多好。
我还注释掉了 while 循环不起作用，因为正式的软件验证工具通常讨厌循环，尤其是无界循环。