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
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
