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

[Balázs Benics via Phabricator via cfe-commits]

steakhal added a comment.

In D90157#2361773 <https://reviews.llvm.org/D90157#2361773>, @ASDenysPetrov wrote:

> 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 ?


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D90157/new/

https://reviews.llvm.org/D90157