This is an archive of the discontinued LLVM Phabricator instance.

[analyzer] Rework SValBuilder::evalCast function into maintainable and clear way
ClosedPublic

Authored by ASDenysPetrov on Oct 26 2020, 7:54 AM.

Details

Summary

Refactor SValBuilder::evalCast function. Make the function clear and get rid of redundant and repetitive code. Unite SValBuilder::evalCast, SimpleSValBuilder::dispatchCast, SimpleSValBuilder::evalCastFromNonLoc and SimpleSValBuilder::evalCastFromLoc functions into single SValBuilder::evalCast.

P.S. Inspired by D89055.

Now I'm going to make unittests for SValBuilder::evalCast. Let me ask you to offer me some examples of casts to check. As many cases we can collect as robust the test would be. E.g.

int x; // case 1
float y;
x = y;

int x; // case 2
(void)x;
...

Diff Detail

Event Timeline

ASDenysPetrov created this revision.Oct 26 2020, 7:54 AM
ASDenysPetrov requested review of this revision.Oct 26 2020, 7:54 AM
ASDenysPetrov edited the summary of this revision. (Show Details)Oct 26 2020, 9:53 AM

Now I'm going to make unittests for SValBuilder::evalCast. Let me ask you to offer me some examples of casts to check. As many cases we can collect as robust the test would be. E.g.

This is not going to be easy. I guess we should cover both implicit and explicit type conversions. C++ is ridiculously complex in these domains. For maximal precision I'd suggest to systematically go through the below pages and try to cover each major case:
https://en.cppreference.com/w/cpp/language/explicit_cast
https://en.cppreference.com/w/cpp/language/implicit_conversion

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
105

+1 for this kind of splitting, makes the code cleaner for me.

Now I'm going to make unittests for SValBuilder::evalCast. Let me ask you to offer me some examples of casts to check. As many cases we can collect as robust the test would be. E.g.

This is not going to be easy. I guess we should cover both implicit and explicit type conversions. C++ is ridiculously complex in these domains. For maximal precision I'd suggest to systematically go through the below pages and try to cover each major case:
https://en.cppreference.com/w/cpp/language/explicit_cast
https://en.cppreference.com/w/cpp/language/implicit_conversion

@martong Keep in mind that we try hard not to emit casts - even if that would require. Check D85528, exactly touching this topic.


By the same token, I think you should run the test-suite using the Z3 refutation and/or Z3 constraint solver to check if this introduces any regression.
You can do that by installing Z3, adding the cmake options: -DLLVM_ENABLE_Z3_SOLVER=ON, -DLLVM_Z3_INSTALL_DIR=/path/to/z3
After this, you should be able to run the lit-test:
./bin/llvm-lit -sv --show-unsupported --show-xfail /home/elnbbea/git/llvm-project/clang/test/Analysis --param USE_Z3_SOLVER=1
Run it before and after your fix and you should expect no new failures/crashes.

ASDenysPetrov added a comment.EditedOct 29 2020, 6:12 AM

Who can confirm if this is correct or somewhere it needs fixes? Here is a generated result of evalCast from the origin branch(before the patch):

void foo(int* x,  // &SymRegion{reg_$0<int * x>}
         int** y, // &SymRegion{reg_$1<int ** y>}
         int***z) // &SymRegion{reg_$2<int *** z>}
{
 (void*)x;    // &SymRegion{reg_$0<int * x>}
 (void*)y;    // &SymRegion{reg_$1<int ** y>}
 (void*)z;    // &SymRegion{reg_$2<int *** z>}
 (void**)x;   // &Element{SymRegion{reg_$0<int * x>},0 S64b,void *}
 (void**)y;   // &SymRegion{reg_$1<int ** y>}
 (void**)z;   // &SymRegion{reg_$2<int *** z>}
 (void***)x;  // &Element{SymRegion{reg_$0<int * x>},0 S64b,void **}
 (void***)y;  // &Element{SymRegion{reg_$1<int ** y>},0 S64b,void **}
 (void***)z;  // &SymRegion{reg_$2<int *** z>}
 (void****)x; // &Element{SymRegion{reg_$0<int * x>},0 S64b,void ***}
 (void****)y; // &Element{SymRegion{reg_$1<int ** y>},0 S64b,void ***}
 (void****)z; // &Element{SymRegion{reg_$2<int *** z>},0 S64b,void ***}
}

@martong

https://en.cppreference.com/w/cpp/language/explicit_cast
https://en.cppreference.com/w/cpp/language/implicit_conversion

Thanks for the links.
@steakhal

By the same token, I think you should run the test-suite using the Z3 refutation and/or Z3 constraint solver to check if this introduces any regression.

Never worked with Z3 before. I'll try.

Who can confirm if this is correct or somewhere it needs fixes? Here is a generated result of evalCast from the origin branch(before the patch):

void foo(int* x,  // &SymRegion{reg_$0<int * x>}
         int** y, // &SymRegion{reg_$1<int ** y>}
         int***z) // &SymRegion{reg_$2<int *** z>}
{
 (void*)x;    // &SymRegion{reg_$0<int * x>}
 (void*)y;    // &SymRegion{reg_$1<int ** y>}
 (void*)z;    // &SymRegion{reg_$2<int *** z>}
 (void**)x;   // &Element{SymRegion{reg_$0<int * x>},0 S64b,void *}
 (void**)y;   // &SymRegion{reg_$1<int ** y>}
 (void**)z;   // &SymRegion{reg_$2<int *** z>}
 (void***)x;  // &Element{SymRegion{reg_$0<int * x>},0 S64b,void **}
 (void***)y;  // &Element{SymRegion{reg_$1<int ** y>},0 S64b,void **}
 (void***)z;  // &SymRegion{reg_$2<int *** z>}
 (void****)x; // &Element{SymRegion{reg_$0<int * x>},0 S64b,void ***}
 (void****)y; // &Element{SymRegion{reg_$1<int ** y>},0 S64b,void ***}
 (void****)z; // &Element{SymRegion{reg_$2<int *** z>},0 S64b,void ***}
}

AFAIK, Element regions represent the reinterpret casts, and static-casts doesn't require anything to do as the loading from the region would be cast to the appropriate type.
So these dumps seem to be correct.

BTW, this dispatching logic should be done with an SValVisitor IMO. That way you could make it even more cleaner. @ASDenysPetrov

@steakhal

By the same token, I think you should run the test-suite using the Z3 refutation and/or Z3 constraint solver to check if this introduces any regression.

Never worked with Z3 before. I'll try.


I've run the baseline and your patch as well on 15 projects, both with and without Z3 refutation enabled.

The reports for these 13 projects did not change at all:

Bitcoin_v0.20.1
Curl_curl-7_66_0
Memchached_1.6.8
OpenSSL_openssl-3.0.0-alpha7
PostgreSQL_REL_13_0
Redis_5.0.6
SQLite_version-3.33.0
TinyXML2_8.0.0
Vim_v8.2.1920
Xerces_v3.2.3
libWebM_libwebm-1.0.0.27
protobuf_v3.13.0
tmux_3.0

However, for twin, it introduced a new unique report:

server/socketalien.h @ Line 64	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound

And for the FFMPEG, 2 unique reports were lost without Z3 refutation:

vf_edgedetect.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
mpc8.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound

3 unique reports were lost with Z3 refutation:

utvideodec.c 	7th function call argument is an uninitialized value 	core.CallAndMessage
utvideodec.c 	The left operand of '-' is a garbage value 	core.UndefinedBinaryOperatorResult
xan.c 	Arguments must not be overlapping buffers 	alpha.unix.cstring.BufferOverlap

And introduced 35 unique new ones without Z3 refutation, only 34 with refutation:

lpc.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound   (Z3 refutation filters this)
on2avc.c 	Memory copy function accesses out-of-bound array element 	alpha.unix.cstring.OutOfBounds
bytestream.h 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
ws-snd1.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
des.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
012v.c 	Memory copy function accesses out-of-bound array element 	alpha.unix.cstring.OutOfBounds
012v.c 	Memory copy function accesses out-of-bound array element 	alpha.unix.cstring.OutOfBounds
brenderpix.c 	Division by zero 	core.DivideZero
h264_cavlc.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264_cavlc.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
bytestream.h 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
rtpenc_h263.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
rtpenc_h263.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
avc.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound

All in all, I'm still in favor of this change, but I'm really curious why did we observe such changes. Debugging the cause seems really tricky to me.
Maybe dumping the exploded graph in both cases and diffing them could show something useful to narrow this down the problem space to a pair of states.
What do you think @ASDenysPetrov ?

@steakhal
Thank you for your invaluable analysis!

What do you think @ASDenysPetrov ?

I think if there is any difference then I have to inspect the changes deeper. I tryed to make this changes in a way of not changing any behaviour.
Let me back to this patch a bit later. Currently have another important task.

@steakhal
I've precisely inspected your reports and find the bug. I've fixed it. I also verified all the rest and find some other vulnerabilities and fixed them as well.
Thank you for your testing, and I would ask you to run these tests again on my fix.

ASDenysPetrov added a comment.EditedDec 22 2020, 3:25 AM

Thank to @steakhal for the new tests.
All previous result differences have gone in FFMPEG and twin but a new one appeared in PostgreSQL.

/src/common/d2s.c  Line 895 Memory copy function overflows the destination buffer alpha.unix.cstring.OutOfBounds

Here is an original link to the report: https://codechecker-demo.eastus.cloudapp.azure.com/Default?run=D90157&items-per-page=100 (login: demo, pass: demo)

I'm going to work on the patch to remove this single difference.

Unfortunately I wasn't able to reproduce the singe difference in PostgreSQL project. So I revised the patch in a part of the difference nature.
This update passed all of CodeChecker's tests without any difference.
So for now the patch looks like ready to be accepted.
Please, welcome for review.

Please @ASDenysPetrov, give full context with the option -U99999999 when you export the diff from git.
I would like to quickly swipe through the code before I accept this.

@steakhal
Oh, sure. Updated.

What you are basically doing is a visitation on the kind of the SVal.
Why don't you use the SValVisitor instead? That way you could focus on the leaf nodes in the hierarchy, leaving you an even cleaner solution.

class CastEvaluator : public SValVisitor<CastEvaluator, SVal> {
public:
  CastEvaluator(QualType CastTy, QualType OriginalTy /*etc.*/)
  SVal VisitPointerToMember(nonloc::PointerToMember V) { return V; }
  SVal VisitGotoLabel(loc::GotoLabel V) { /*impl.*/ }
  /* etc. */
};

Comments should be punctuated and the variables should start with an uppercase letter in general.
About the correctness: I think it still needs a bit more confidence. I'm gonna run this on LLVM itself and see if anything changes.

I really like where this is going. Keep up the good work.

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
105–127

Why are all of these public?
I would expect only the first overload to be public.

clang/lib/StaticAnalyzer/Core/SValBuilder.cpp
642–686

Arrays decay to a pointer to the first element, but in this case, you return Unknown.
Why?

675–676

nit

746–750

Just call immediately that lambda and assign that value to a const llvm::APSInt CastedValue.

836–839

Presumably what?

@steakhal

Why don't you use the SValVisitor instead?

I simply didn't know of its exsistence. We can try to transform this patch using SValVisitor in the next revision to make the review easier and avoid additional complexity.

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
105–127

Great catch. I'll do it.

clang/lib/StaticAnalyzer/Core/SValBuilder.cpp
642–686

This is just how evalCast worked before the patch. I didn't think of why. I've just tried to replicate previous cast logic. If I'd change anything, you'd catch a bunch of differences in CodeChecker. That's what I didn't want the most.

675–676

Thanks! I'll check all for the naming rules.

746–750

I just wanted to make this lazy. Otherwise this set of calls will be invoked unnecessarily in some cases. I'd prefer to leave it as it is.

836–839

We assume that this condition presents a type which is opposite to float (aka non-float). But it may happen that it is also opposite to some other types. So naming it non-float could be a bit incomplete and we are dealing with some other type. Yes, I feel this embarrassing. I'll remove (presumably).

steakhal added inline comments.Jan 25 2021, 6:05 AM
clang/lib/StaticAnalyzer/Core/SValBuilder.cpp
642–686

I agree, you should not change any behavior in this patch.

746–750

Maybe rename it then. What about GetCastedValue(x)?

Updated. Naming fixes. Member access changes.

Updated. Naming fixes. Member access changes.

Looks great!

IMO we are sort-of late to commit this into clang-12 with confidence.
We should land it after we tag that release.
What do you think @xazax.hun?

Hi, guys!
Does anyone can review this item, except @steakhal (thanks him)? Please, look.

steakhal accepted this revision.Feb 11 2021, 9:29 AM
This revision is now accepted and ready to land.Feb 11 2021, 9:29 AM
NoQ added a comment.Apr 8 2021, 10:59 AM

I'm catching up and these changes look great.

I've run the baseline and your patch as well on 15 projects, both with and without Z3 refutation enabled.
(...)
All in all, I'm still in favor of this change, but I'm really curious why did we observe such changes. Debugging the cause seems really tricky to me.

If testing on a large codebase uncovered changes in behavior that weren't caught by our LIT test suite it often make sense to update our LIT test suite to include those tests in order to avoid similar regressions in the future. Regressions like this are easy to auto-reduce with tools like creduce because there's no functional change intended in the patch so there's a 100% formal reduction criterion "any change in diagnostics is observed" which can be easily fed to creduce. Even though NFC commits don't require tests, this doesn't mean they shouldn't add them!

@NoQ

Even though NFC commits don't require tests, this doesn't mean they shouldn't add them!

While developing this, I wasn't able to reproduce any regression or unpassed cases on the projects from CodeChecker list (Bitcoin_v0.20.1, Curl_curl-7_66_0, Memchached_1.6.8, OpenSSL_openssl-3.0.0-alpha7, etc.) due to my platform. I use Windows and those projects either don't compile or need hard effort to set them up.
But anyway I was able to detect some different diagnostics in existing tests casts.cpp using Z3 refutation option. That actually helped to make corrections.