Exception on `--smt2`

[nchong]

The following program makes CBMC throw an exception when using the switch --smt2: Unexpected case: smt2_convt::convert_expr: ``function_application' is unsupported. The program is parsed and fails verification (as expected) when --smt2 is removed.

int __CPROVER_uninterpreted_func(int);
int main() {
  int x = __CPROVER_uninterpreted_func(42);
  __CPROVER_assert(0 == 1, "Always fail");
}

Here's the full output:

$ cbmc --smt2 example.c
CBMC version 5.8 64-bit x86_64 macos
Parsing bad.c
Converting
Type-checking bad
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 34 steps
simple slicing removed 5 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to SMT2 QF_AUFBV using Z3
converting SSA
Unexpected case: smt2_convt::convert_expr: `function_application' is unsupported

[karkhaz]

@nchong using a non-__CPROVER prefixed name for the function makes this problem go away:

$ cat /tmp/example.c
int foo(int);
int main() {
  int x = foo(42);
  __CPROVER_assert(0 == 1, "Always fail");
}
$ cbmc --smt2 /tmp/example.c
CBMC version 5.8 64-bit x86_64 linux
Parsing /tmp/foo.cpp
Converting
Type-checking foo
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
**** WARNING: no body for function foo(signed_int)
size of program expression: 34 steps
simple slicing removed 5 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to SMT2 QF_AUFBV using Z3
converting SSA
Running SMT2 QF_AUFBV using Z3
decision procedure has failed
Runtime decision procedure: 0.0104346s

** Results:
[main.assertion.1] Always fail: ERROR


** 0 of 1 failed (1 iteration)

is there a reason why you're calling your function __CPROVER_uninterpreted_function? That doesn't seem to be a name that CBMC has reserved for a specific use, but it's best to avoid naming functions that way even so...if there's a good reason to be using that name I can ping somebody, otherwise please use a different name.

[karkhaz]

Actually, I'm going to ping somebody anyway. @peterschrammel is there a reason why CBMC behaves differently in the presence of __CPROVER-prefixed functions even when those names haven't been reserved by CBMC? It seems to me that either the behaviour should be identical to a regular function, or CBMC should be warning users that they're using a name which isn't reserved but which will change the verification behaviour...

If nothing else, it would be helpful to warn about unknown __CPROVER-prefixed identifiers so that users get warned when they accidentally write __CPROVER_assune instead of __CPROVER_assume.

[nchong]

Thanks for the response, @karkhaz. My understanding is that the prefix __CPROVER_uninterpreted_ causes the function to be treated as an uninterpreted function.

http://www.cprover.org/cprover-manual/modeling-nondet.shtml

[karkhaz]

Ah, I see, thanks! (I was grepping for uninterpreted_function rather than uninterpreted_...) in which case, not sure about this, but perhaps @peterschrammel knows who would best know more about this part of the codebase...

[polgreen]

The manual does say that this feature isn't supported on all back ends, hence the error message. Admittedly the error message could be a bit clearer. As far as I can tell, the only back end with which CBMC currently supports uninterpreted functions is minisat.

There doesn't seem to be a reason that it couldn't be supported by the smt back end, since Z3 has support for uninterpreted functions, just that the conversion to smt output hasn't been written yet. So I guess this is a feature request, rather than a bug report?

[martin-cs]

@polgreen Yes; should be easy to support in the SMT-LIB back-end; I think the key change will be making sure that the function is declared properly before use in the SMT.

[nchong]

@polgreen @martin-cs Thanks very much for your comments. If this is a relatively easy feature to implement then I would find it very useful.

Will uninterpreted function calls have a different expr.id? Maybe we could add the uninterpreted function call declarations in the smt2 header? If one of you had time to give me an overview of solvers/smt2/smt2_conv.cpp then I'd be happy to try implementing this myself.

[martin-cs]

@nchong I would be (unpleasently) surprised if it is more than a day's work. If it is then we should stop and think about why and whether there is a better way. Hypothetically, one would need to...

function_application is the key type. One place they are built (the one you are probably using) is here:

https://github.com/diffblue/cbmc/blob/develop/src/goto-programs/builtin_functions.cpp#L916

As for solvers/smt2/smt2_conv.cpp (paging @owen-jones-diffblue for documentation related activities), the go bit is dec_solve():

https://github.com/diffblue/cbmc/blob/develop/src/solvers/smt2/smt2_conv.h#L102

However, you will probably care more about convert`` and set_*``` which are the entry points to function conversion.

https://github.com/diffblue/cbmc/blob/develop/src/solvers/smt2/smt2_conv.h#L109

convert illustrates the general approach best:

https://github.com/diffblue/cbmc/blob/develop/src/solvers/smt2/smt2_conv.cpp#L710

One pass with find_symbols to declare things before they are used, then call convert_expr which will actually generate the expression. (set_to is basically an optimisation of this for things of the form new_variable = expression).

( Task -1 : Create one or more regression tests. These may have to be separate for now as at the moment we don't (but should!) run SMT solver as part of the regression tests -- fixing this is beyond the scope of this PR. )

( Task 0 : Add UF to the theory. )

Task 1 : Get find_symbols to generate uninterpreted functions. The key problem is the symbols are always treated as 0-artiy functions, here:

https://github.com/diffblue/cbmc/blob/develop/src/solvers/smt2/smt2_conv.cpp#L4201

you may well have to hack convert_type which does the obvious thing.

Task 2 : Add a case to the end of convert_expr which avoids the current exception and handles ID_function_application :

https://github.com/diffblue/cbmc/blob/develop/src/solvers/smt2/smt2_conv.cpp#L1868

Task 3 : Parsing the resultant models I'll leave as an exercise for you!

Does that tempt you? :-)

[nchong]

@martin-cs Thanks for the pointers. I'd be happy to give this a go. I may check back in with you with some further questions, but it looks straightforward (at present)!

• Will the declaration of the uninterpreted function be represented as an expr? If so then what will its id() be: ID_symbol?

[nchong]

@martin-cs I've made some progress here: https://github.com/nchong/cbmc/tree/smt2_uf

Task -1: Added regressions to regression/smt2_solver/uninterpreted_function[1-4]/
Task 0: This wasn't necessary because it seems that we are already using QF_AUFBV
Task 1: This one is the difficult one. I wasn't able to figure out how to extract out the declarations of the uninterpreted functions (since I need the types of the arguments as well as the return type). Instead, I look at the function applications themselves. And, if they match an uninterpreted function call (which we have not emitted yet) then an smt2 function is declared. I think you had a better way in mind. Can you comment on how to do this properly?
Task 2: Done in convert_expr

Also, regression/smt2_solver/uninterpreted_function1 is giving me an error Assertion failed: (expr.id()==ID_symbol && expr.get_bool(ID_C_SSA_symbol) && !expr.has_operands()), function to_ssa_expr, file ../util/ssa_expr.h, line 158. which I will follow-up.

Thanks for your guidance so far!

[tautschnig]

This was fixed in cace2ce (#6709), which is included in 5.53.0 as well as any later version.

[sdivakarank]

I have an issue in using an SMT solver in CBMC.
When I am using the command:
CBMC --z3 sample.c
it is giving the following response after it generates SSA form

Running SMT2 QF_AUFBV using Z3
decision procedure has failed
Runtime decision procedure: 0.003s

** Results:
[foo.assertion.1] assertion i <= a && res == b + i: ERROR

The same message I am getting when I am using any solver other than the default one.

Can someone help me how to solve this issue?

[martin-cs]

@sdivakarank Would you mind opening a separate issue for this? Given how people on the project work, comments on a closed issue are likely to be missed.

Things to try:

• Is Z3 installed and the path set up correctly?
• If you generate to a file using --outfile sample.smt2 and run your SMT solver of choice on it, what do you get?