Fix crashes in z3 by Ken-Patrick · Pull Request #2203 · cppcheck-opensource/cppcheck

Ken-Patrick · 2019-09-22T18:56:23Z

http://cppcheck1.osuosl.org:8000/z3

2019-09-22 03:00
ftp://ftp.se.debian.org/debian/pool/main/z/z3/z3_4.8.4.orig.tar.gz
cppcheck-options: -j1 --library=posix --library=gnu --library=openmp -D__GNUC__ --check-library --inconclusive --enable=style,information --platform=unix64 --template=daca2 -rp=temp temp
platform: Linux-4.15.0-64-generic-x86_64-with-Ubuntu-18.04-bionic
python: 2.7.15+
client-version: 1.1.37
cppcheck: head 1.89
head-info: 6c9839a58 (2019-09-21 21:42:13 +0200)
count: Crash! Crash!
elapsed-time: -11.0 -11.0
head results:
Checking temp/z3-z3-4.8.4/src/nlsat/nlsat_explain.cpp: __GNUC__=1...

Program received signal SIGSEGV, Segmentation fault.
singleMemberCallInScope (start=start@entry=0x555555e76750, varid=397, input=@0x7fffffffb25e: false) at build/checkstl.cpp:3976
3976	    if (isVariableChanged(dotTok->next(), endStatement, dotTok->astOperand1()->varId(), false, nullptr, true))
 #0  singleMemberCallInScope (start=start@entry=0x555555e76750, varid=397, input=@0x7fffffffb25e: false) at build/checkstl.cpp:3976
 #1  0x000055555566d0c5 in CheckStl::useStlAlgorithm (this=this@entry=0x7fffffffb390) at build/checkstl.cpp:4144
 #2  0x000055555567d6ed in CheckStl::runChecks (this=<optimized out>, tokenizer=<optimized out>, settings=0x7fffffffcd50, errorLogger=0x7fffffffcb30) at lib/checkstl.h:74
 #3  0x00005555556a9150 in CppCheck::checkNormalTokens (this=this@entry=0x7fffffffcb30, tokenizer=...) at build/cppcheck.cpp:732
 #4  0x00005555556adb6e in CppCheck::checkFile (this=this@entry=0x7fffffffcb30, filename="temp/z3-z3-4.8.4/src/nlsat/nlsat_explain.cpp", cfgname="", fileStream=...) at build/cppcheck.cpp:542
 #5  0x00005555556b18bc in CppCheck::check (this=this@entry=0x7fffffffcb30, path="temp/z3-z3-4.8.4/src/nlsat/nlsat_explain.cpp") at build/cppcheck.cpp:197
 #6  0x0000555555809337 in CppCheckExecutor::check_internal (this=this@entry=0x7fffffffd8c0, cppcheck=..., argv=argv@entry=0x7fffffffdc48) at cli/cppcheckexecutor.cpp:884
 #7  0x0000555555809c6a in CppCheckExecutor::check (this=0x7fffffffd8c0, argc=14, argv=0x7fffffffdc48) at cli/cppcheckexecutor.cpp:198
 #8  0x00005555555b899b in main (argc=14, argv=0x7fffffffdc48) at cli/main.cpp:95

Due to code like the following, when cppcheck does not have the macros
DEBUG_CODE or TRACE defined:

        DEBUG_CODE(
                TRACE("nlsat",
                      for (literal l : result) {
                          m_solver.display(tout << " ", l);
                      }
                      tout << "\n";
                      );
                for (literal l : result) {
                    CTRACE("nlsat", l_true != m_solver.value(l), m_solver.display(tout, l) << " " << m_solver.value(l) << "\n";);
                    SASSERT(l_true == m_solver.value(l));
                });

I couldn't get a small reproducer, though.

danmar · 2019-09-22T19:24:00Z

I think it would be preferable to throw an unknownMacro exception early.. do you think that is possible somehow.. maybe if there is something like :

SOME_UPPERCASE_NAME( .. for .. )

danmar · 2019-09-22T19:25:54Z

We throw unknownMacro exceptions in Tokenizer if we see some incomplete code...

Ken-Patrick · 2019-09-22T20:12:48Z

I think it would be preferable to throw an unknownMacro exception early.. do you think that is possible somehow.. maybe if there is something like :
SOME_UPPERCASE_NAME( .. for .. )

Ok, I'll try that.

http://cppcheck1.osuosl.org:8000/z3 ``` 2019-09-22 03:00 ftp://ftp.se.debian.org/debian/pool/main/z/z3/z3_4.8.4.orig.tar.gz cppcheck-options: -j1 --library=posix --library=gnu --library=openmp -D__GNUC__ --check-library --inconclusive --enable=style,information --platform=unix64 --template=daca2 -rp=temp temp platform: Linux-4.15.0-64-generic-x86_64-with-Ubuntu-18.04-bionic python: 2.7.15+ client-version: 1.1.37 cppcheck: head 1.89 head-info: 6c9839a (2019-09-21 21:42:13 +0200) count: Crash! Crash! elapsed-time: -11.0 -11.0 head results: Checking temp/z3-z3-4.8.4/src/nlsat/nlsat_explain.cpp: __GNUC__=1... Program received signal SIGSEGV, Segmentation fault. singleMemberCallInScope (start=start@entry=0x555555e76750, varid=397, input=@0x7fffffffb25e: false) at build/checkstl.cpp:3976 3976 if (isVariableChanged(dotTok->next(), endStatement, dotTok->astOperand1()->varId(), false, nullptr, true)) #0 singleMemberCallInScope (start=start@entry=0x555555e76750, varid=397, input=@0x7fffffffb25e: false) at build/checkstl.cpp:3976 #1 0x000055555566d0c5 in CheckStl::useStlAlgorithm (this=this@entry=0x7fffffffb390) at build/checkstl.cpp:4144 cppcheck-opensource#2 0x000055555567d6ed in CheckStl::runChecks (this=<optimized out>, tokenizer=<optimized out>, settings=0x7fffffffcd50, errorLogger=0x7fffffffcb30) at lib/checkstl.h:74 cppcheck-opensource#3 0x00005555556a9150 in CppCheck::checkNormalTokens (this=this@entry=0x7fffffffcb30, tokenizer=...) at build/cppcheck.cpp:732 cppcheck-opensource#4 0x00005555556adb6e in CppCheck::checkFile (this=this@entry=0x7fffffffcb30, filename="temp/z3-z3-4.8.4/src/nlsat/nlsat_explain.cpp", cfgname="", fileStream=...) at build/cppcheck.cpp:542 cppcheck-opensource#5 0x00005555556b18bc in CppCheck::check (this=this@entry=0x7fffffffcb30, path="temp/z3-z3-4.8.4/src/nlsat/nlsat_explain.cpp") at build/cppcheck.cpp:197 cppcheck-opensource#6 0x0000555555809337 in CppCheckExecutor::check_internal (this=this@entry=0x7fffffffd8c0, cppcheck=..., argv=argv@entry=0x7fffffffdc48) at cli/cppcheckexecutor.cpp:884 cppcheck-opensource#7 0x0000555555809c6a in CppCheckExecutor::check (this=0x7fffffffd8c0, argc=14, argv=0x7fffffffdc48) at cli/cppcheckexecutor.cpp:198 cppcheck-opensource#8 0x00005555555b899b in main (argc=14, argv=0x7fffffffdc48) at cli/main.cpp:95 ``` Due to code like the following, when cppcheck does not have the macros `DEBUG_CODE` or `TRACE` defined: ``` DEBUG_CODE( TRACE("nlsat", for (literal l : result) { m_solver.display(tout << " ", l); } tout << "\n"; ); for (literal l : result) { CTRACE("nlsat", l_true != m_solver.value(l), m_solver.display(tout, l) << " " << m_solver.value(l) << "\n";); SASSERT(l_true == m_solver.value(l)); }); ```

Ken-Patrick · 2019-10-08T07:31:10Z

I think it would be preferable to throw an unknownMacro exception early.. do you think that is possible somehow.. maybe if there is something like :
SOME_UPPERCASE_NAME( .. for .. )

Similarly to #2236, wouldn't it be better to keep cppcheck able to cope with incomplete code as best as it can ?
I have found a small reproducer and added it in the unit tests. Also, I've provided a smaller and hopefully better fix.

danmar · 2019-10-08T08:17:47Z

Similarly to #2236, wouldn't it be better to keep cppcheck able to cope with incomplete code as best as it can ?

That is mostly the goal.

If the code follows C/C++ syntax rules.. and there are just missing declarations.. we should handle the code anyway. Missing variables/types/functions/templates/constants/etc is fine. Unseen macro definitions are not a problem as long as the usage follows the normal C/C++ syntax rules. If you have a function-like macro that will work. A macro that evaluates to some constant value will work. etc..

If the code has bad syntax because of macros.. then we just can't build a symboldatabase or ast that is even close enough.

an alternative here might be to convert MACRO(..for..) into asm(""). The analysis will be skipped mostly for this then. Probably there will be some type checks but no valueflow-related analysis will be executed. Well it could be done but I would suggest that the user is highly recommended to ensure that MACRO is defined anyway.

If we do want to run some checkers even on code that has "bad syntax"... it could be done in the past so it is not impossible. But we can't rely on ast nor symboldatabase then. The checks that rely only on token pattern matching could still be used. However we do not have many such checks anymore. We have converted many checks to use ast/symboldatabase because it simplify and improve the checks.
In the past we used to have "Token simplifications" .. this is code that I do not want to reintroduce.

Ken-Patrick · 2019-10-08T08:22:48Z

Ok, thanks for the clarification. I see better the direction we want to take.

danmar · 2019-11-03T09:11:26Z

I close this

Ken-Patrick force-pushed the z3 branch from c999c1e to 172cd2d Compare October 8, 2019 07:28

danmar closed this Nov 3, 2019

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix crashes in z3#2203

Fix crashes in z3#2203
Ken-Patrick wants to merge 1 commit into
cppcheck-opensource:masterfrom
Ken-Patrick:z3

Ken-Patrick commented Sep 22, 2019

Uh oh!

danmar commented Sep 22, 2019

Uh oh!

danmar commented Sep 22, 2019

Uh oh!

Ken-Patrick commented Sep 22, 2019

Uh oh!

Ken-Patrick commented Oct 8, 2019

Uh oh!

danmar commented Oct 8, 2019

Uh oh!

Ken-Patrick commented Oct 8, 2019

Uh oh!

danmar commented Nov 3, 2019

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

Ken-Patrick commented Sep 22, 2019

Uh oh!

danmar commented Sep 22, 2019

Uh oh!

danmar commented Sep 22, 2019

Uh oh!

Ken-Patrick commented Sep 22, 2019

Uh oh!

Ken-Patrick commented Oct 8, 2019

Uh oh!

danmar commented Oct 8, 2019

Uh oh!

Ken-Patrick commented Oct 8, 2019

Uh oh!

danmar commented Nov 3, 2019

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants