是否可以将C++代码转换为SMT2？

问题描述 投票：0回答：2

我是 SMT 求解器和这些主题的新手。我需要将 C++ 代码转换为 SMT2 的等效代码（我有一个需要 .smt2 作为输入的工具）。我已经找到了这个解决方案，但它没有完全解释如何做到这一点？你能帮我一下吗？谢谢

while (x<y)
{
x=5*x+3; 
y=3*y+5; 
w=3*z+w; 
z=z+6;
}

有没有什么工具可以进行这种转换？或者我应该如何了解这个主题？

z3 smt
2个回答
1
投票

如果您正在寻找一个可以将任意 C++ 转换为 SMTLib 的工具，那么我认为这样的工具不存在，也不可行，因为这意味着您需要非常精确的 C++ 语义在 SMTLib 中编码，即使不是不可能，也是一项艰巨的任务。

如果您关心有限的子集，或者只想手动翻译一两个具体示例，那么您找到的答案就很好。首先研究SMTLib本身，并查找SSA（单一静态分配）。循环会很困难，但有一些方法可以处理它们。同样，这完全取决于您到底想要实现什么目标。一旦您查看了这些选项，也许您可以提出更具体的问题。

0
投票

这样做也不可行

这是可行的。 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)

那是因为我们告诉它只验证

foo
，并且那里确实没有什么需要验证的（没有断言）。如果我们告诉它用断言验证一个函数（即 
main
，这是默认函数），那么它将生成一些 SMT2：

❯ 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 循环不起作用，因为正式的软件验证工具通常讨厌循环，尤其是无界循环。

最新问题
© www.soinside.com 2019 - 2024. All rights reserved.