Is that possible to convert a C++ code to SMT2?

Question

I am new to SMT solver and these topics. I need to convert a C++ code into an equivalent of SMT2 (I have a tool that needs .smt2 as input). I've already found this solution but it does not explain completely how to do that? Could you help me. Thanks

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

Is there any kind of tool for this conversion? or how should I learn about this topic?

Answer 1

nor it would be feasible to do so

It is feasible. CBMC can do it. The slightly annoying thing is it doesn't output SMT2 for functions that aren't "used". Consider this program:

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);
}

You can verify it like this:

❯ 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

You can tell it to generate smt2 like this:

❯ 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

However if you check the file it is empty:

❯ 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)

That's because we told it to only verify foo, and there's really nothing to verify in there (no asserts). If we tell it to verify a function with an assert (i.e. main which is the default function) then it will generate some 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

Hopefully that helps. Tbh I haven't really used this yet so I don't know how good the output is.

Also I commented out the while loop doesn't work because formal software verification tools generally hate loops, especially unbounded ones.

Answer 2

If you're looking for a tool that can convert arbitrary C++ to SMTLib, then I don't believe such a tool exists, nor it would be feasible to do so for that would mean you'd need a very precise semantics of C++ encoded in SMTLib, a gargantuan task if not impossible.

If you care about a restricted subset, or just want to hand-translate one-or two specific examples, then the answer you found is as good as it's going to get. Start by studying SMTLib itself, and look up SSA (single static-assignment). Loops will be difficult, but there are ways to deal with them. Again, it all depends on what exactly you're trying to achieve. Once you look at these options, perhaps you can ask a more specific question.