Bug-Hunting: Uses all Memory when analyzing project cntlm

[versat]

I tested --bug-hunting on a project I am working on.
When analyzing the file xcrypt.c Cppcheck uses all RAM when --bug-hunting is enabled.
To reproduce this it is enough to download xcrypt.c and xcrypt.h and run ./cppcheck --bug-hunting xcrypt.c.
On my PC after nearly a minute all the RAM is used. Tested on Windows 7, compiled with Visual Studio 2019.

[Daniel Marjamäki]

hmm.. did you link with z3? should z3 be optional or required in visual studio? to me it would seem fine to include the z3.dll in the repo and always use that. if you want .. feel free to update the visual studio solution.

[versat]

I did not link with z3. I knew that it can be used but do not know much about it. Would you expect a drastic performance improvement with the z3 library?
I guess this is the correct repository: https://github.com/Z3Prover/z3
The libz3.dll for x64 is about 14 MB in size. We would need the libz3.dll for x86 too I guess. IMHO this is a bit too much for committing it to the Cppcheck repository.
The includes are "only" some hundred KB, that would be acceptable I guess.
Hmm, not sure if it makes sense to add it to the repo, and if how to best integrate it into the VS project.

[Daniel Marjamäki]

I do not expect any performance improvement at all. I believe that the results without z3 will be much more unreliable.

ok adding 2 14 MB dll files to the repo is not optimal. Let's not do that.

Yes it's the https://github.com/Z3Prover/z3 project we want to use.

[versat]

Ok.

I have installed libz3-4 and libz3-dev under Debian 10.1 and tried to compile Cppcheck HEAD with USE_Z3=yes.
I get this error:

g++ -Ilib -isystem externals -isystem externals/simplecpp -isystem externals/tinyxml -DUSE_Z3  -pedantic -Wall -Wextra -Wcast-qual -Wno-deprecated-declarations -Wfloat-equal -Wmissing-declarations -Wmissing-format-attribute -Wno-long-long -Wpacked -Wredundant-decls -Wundef -Wno-shadow -Wno-missing-field-initializers -Wno-missing-braces -Wno-sign-compare -Wno-multichar -D_GLIBCXX_DEBUG -g -std=c++0x  -c -o lib/exprengine.o lib/exprengine.cpp
lib/exprengine.cpp: In member function ‘z3::expr ExprData::addFloat(const string&)’:
lib/exprengine.cpp:602:30: error: ‘class z3::context’ has no member named ‘fpa_const’; did you mean ‘int_const’?
         z3::expr e = context.fpa_const(name.c_str(), 11, 53);
                              ^~~~~~~~~
                              int_const
lib/exprengine.cpp: In member function ‘z3::expr ExprData::getExpr(const ExprEngine::BinOpResult*)’:
lib/exprengine.cpp:620:24: error: could not convert ‘(((int)op1.z3::expr::<anonymous>.z3::ast::operator bool()) % ((int)op2.z3::expr::<anonymous>.z3::ast::operator bool()))’ from ‘int’ to ‘z3::expr’
             return op1 % op2;
                    ~~~~^~~~~
lib/exprengine.cpp: In member function ‘z3::expr ExprData::getExpr(ExprEngine::ValuePtr)’:
lib/exprengine.cpp:649:67: error: call of overloaded ‘int_val(int64_t)’ is ambiguous
                 return context.int_val(int64_t(intRange->minValue));
                                                                   ^
In file included from lib/exprengine.cpp:32:
/usr/include/z3++.h:1737:17: note: candidate: ‘z3::expr z3::context::int_val(int)’
     inline expr context::int_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
                 ^~~~~~~
/usr/include/z3++.h:1738:17: note: candidate: ‘z3::expr z3::context::int_val(unsigned int)’
     inline expr context::int_val(unsigned n) { Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
                 ^~~~~~~
/usr/include/z3++.h:1739:17: note: candidate: ‘z3::expr z3::context::int_val(long long int)’
     inline expr context::int_val(__int64 n) { Z3_ast r = Z3_mk_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
                 ^~~~~~~
/usr/include/z3++.h:1740:17: note: candidate: ‘z3::expr z3::context::int_val(long long unsigned int)’
     inline expr context::int_val(__uint64 n) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
                 ^~~~~~~
make: *** [Makefile:497: lib/exprengine.o] Error 1

Do I have to use a specific Version of z3 or do you have any idea what breaks the build?
In Travis building Cppcheck with z3 seems to be not checked yet, that could be useful.

[Daniel Marjamäki]

I am not sure. I thought that was available in latest Z3.

Personally, I have cloned the Z3 repo and built the library myself. It would be very unfortunate if that is required.

[Daniel Marjamäki]

Maybe we can allow that Z3 without floating point support is compiled also.

[Daniel Marjamäki]

Versat: I made a small fix so you can use "old" Z3. You should be able to compile with this command:

make USE_Z3=yes CPPFLAGS="-DUSE_Z3 -DOLD_Z3"

Personally, I have cloned the Z3 repo and built the library myself. It would be very unfortunate if that is required.

no I was wrong, I've installed with apt-get and it worked somehow. hmm.. I use debian also.

[Paul Fultz]

We should treat z3 as external dependency just like libpcre. This is listed in the requirments.txt file so then cppcheck can be built with just cget build( and it will build the corresponding dependencies). Adding Z3Prover/z3 to requirements.txt will build and install z3 as well, we just need to update cmake to call find_package(Z3).

I usually use this to install cppcheck locally on machines. I can install a specific version with cget install danmar/cppcheck@1.90 or install from a commit hash with cget install danmar/cppcheck@fddc301f7b334fd06f7cfd65ff952d8a5301a74e.

Ideally, we could use cget to build cppcheck on daca@home since it can be easily installed with python(ie pip install cget) and it is portable on windows as well. The only issue is that z3 takes little time to build so might want to use something like ccache or only build the dependencies when thay change.

[Daniel Marjamäki]

yes z3 should be a external dependency.

if somebody wants to use cget, no matter platform, that is fine to me.

I'd personally prefer to use native tools, like apt-get.

I don't know how we best add z3 in the visual studio. Isn't vcpkg integrated directly in VS somehow?

[Daniel Marjamäki]

We should treat z3 as external dependency just like libpcre. This is listed in the requirments.txt file so then cppcheck can be built with just cget build( and it will build the corresponding dependencies). Adding Z3Prover/z3 to requirements.txt will build and install z3 as well, we just need to update cmake to call find_package(Z3).

Feel free to update requirements.txt/cmake/etc.. sounds like you know this stuff much better than I do.

[Daniel Marjamäki]

Versat: Now, you should be able to compile like so:

make USE_Z3=yes

The OLD_Z3 was removed and a NEW_Z3 was added in case anybody wants to use that. It turned out I did not have libz3-dev installed. So the header/library I used was something I had compiled myself. I removed my files and installed libz3-dev so my system will use the normal libz3-dev library.

[versat]

Thanks.
make USE_Z3=yes works now for me.
And analyzing my project also works with z3 now.

Maybe there is something that could be improved when not using z3.
Without z3 analyzing xcrypt.c uses all memory and then prints this error:

Checking ../cntlm_versat/xcrypt.c ...
Verify: Aborted analysis of function 'gl_des_ecb_crypt': std::bad_alloc
Checking ../cntlm_versat/xcrypt.c: _STRING_ARCH_unaligned=0...

If you want to have a look at the function gl_des_ecb_crypt() you can view it here:
https://github.com/versat/cntlm/blob/ccf44bd040bd7d653e0f53029b688214958fdc3e/xcrypt.c#L522
It uses several macros. The xcrypt.c file initially was created by the FSF when I read the header comment correctly. Maybe similar code exists also in other open source software.

[versat]

I created a ticket for (what I think is) a false positive: https://trac.cppcheck.net/ticket/9583 (False positive: Bug Hunting: verificationDivByZero for sizeof(), but can not be 0)

Hmm. The error id verificationDivByZero has still verification in its name.
Maybe that should be changed too?

[Daniel Marjamäki]

Maybe there is something that could be improved when not using z3.
Without z3 analyzing xcrypt.c uses all memory and then prints this error:

ok I might look at that if I get some time. I am surprised that z3 prevents the problem.

I created a ticket for (what I think is) a false positive: https://trac.cppcheck.net/ticket/9583 (False positive: Bug Hunting: verificationDivByZero for sizeof(), but can not be 0)

I also think that's a FP. However I thought I already had fixed it with c79ec9e9563ad8a7bc6b53563859ba6676def752. Can you please update and recheck if you still get the false positives?

[versat]

I closed the ticket. You were right, I was somehow using not the latest compiled code. sizeof() does no longer issue these false positives.