search

diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
853 stars 265 forks source link

Troubles while generating SMT2 specification #352

Closed kooshanabedian closed 2 years ago

kooshanabedian commented 7 years ago

Hi there,

We have some problems parsing and transforming C files into SMT2 descriptions. Some of these are unprecedented and we believe have emerged after some recent updates. However we can not specifically identify which one.

We ran CBMC with a simple unwinding option of 2 (not involved with unwinding assertions) on fmt source from coreutils-8.23. The goal is to get the program specifications in SMT2. Although the source is not that much long, and it is rather mildly complicated with recursive functions and stuff, but CBMC shoots out by returning a ~30 GB SMT2 file after 3hrs of tedious working. We ran the same setting with DIMACS format which it didn't even bothered giving out a result and failed after SSA conversions. It seems like it can not figure out how to write formulae into a file. We assured that hard disk space is available and the process has enough access for file operation though.

To give you a glimpse of our trail and error, we also ran the same exact settings for wc command which also failed in generating SMT2, and numfmt, which generated a DIMACS file weighting 104 MB but also gave on when it came to SMT2. However, it is not a consistent phenomenon after all. We have successfully generated SMT2 files of 100 MB or less for some of the other sources in that package. Nevertheless, there were cases where we have got a sound SMT2 file before but now it seems that sometimes the returned SMT2 formulae is partial or half-cut, since Z3 complains about parsing those files.

Just asking anyway, is it normal for an SMT2 file to be like multiple Gigabytes? Even though for such a cute, tiny, number of unwinding turns?

tautschnig commented 7 years ago

Hello, Many thanks for your report. Would you be able to present a script that precisely lists the commands you have gone through in this process? As an example, large arrays may cause such huge SMT files, but in order to properly diagnose what is going on it will be necessary to fully reproduce the steps you have undertaken.

kooshanabedian commented 7 years ago

Thank you for your quick response. I've attached two files. fmt.txt which is the actual C source for fmt command which produced the gigantic SMT2 file, and smtF.zip which contains three snapshots from that file representing huge structures of control flow guards (_gotosymex..._) repeating over and over.

After all, I really didn't quite get it, what exactly should I look for in those files. Any further suggestions or recommendations for generating inner step logs, or something to that effect, from CBMC is appreciated. I hope those help for now.

fmt.txt

smtF.zip

tautschnig commented 7 years ago

Would you mind providing the exact command line that you had used in going from fmt.c (which here is fmt.txt) to the SMT file?

kooshanabedian commented 7 years ago

Sure.

cbmc command : cbmc --smt2 --outfile fmt.smt2 fmt.c -I ./coreutils-8.32/src/ -I ./coreutils-8.32/lib/ -I /usr/include --unwind 2

CBMC version 5.6 64-bit x86_64 linux commit ad7d6395cccfe63e6b0541efddd47de5e45856d2 Sat Nov 19 16:37:27 2016 +0000

tautschnig commented 2 years ago

I was able to reproduce the problem based on the above instructions. With current CBMC (5.69.1) this yields:

[...]
Runtime Symex: 21.2662s
size of program expression: 274298 steps
[...]

and then conversion to a SAT or SMT formula requires a lot of disk space (or memory, if not writing the SAT formula do disk). With 274298 symbolic execution steps this behaviour seems unsurprising, and CBMC might simply not be the right tool here, or manual abstraction needs to be performed.