search

Quuxplusone / LLVMBugzillaTest

0 stars 0 forks source link

z3 fatal error while analyzing webkit #40779

Open Quuxplusone opened 5 years ago

Quuxplusone commented 5 years ago
Bugzilla Link PR41809
Status CONFIRMED
Importance P enhancement
Reported by Paulo Matos (pmatos@linki.tools)
Reported on 2019-05-09 02:17:41 -0700
Last modified on 2020-01-16 15:18:55 -0800
Version 8.0
Hardware PC Linux
CC blitzrakete@gmail.com, dcoughlin@apple.com, dgregor@apple.com, erik.pilkington@gmail.com, llvm-bugs@lists.llvm.org, noqnoqneo@gmail.com, richard-llvm@metafoo.co.uk
Fixed by commit(s)
Attachments 0001-Hack-to-avoid-crash-in-WebKit.patch (1967 bytes, text/plain)
Blocks
Blocked by
See also 
During a WebKit (https://webkit.org/) scan-build analysis (8x branch with  -
analyzer-config crosscheck-with-z3=true) I get the following:
$ /home/pmatos/installs/bin/clang-8 -cc1 -triple x86_64-unknown-linux-gnu -
analyze -disable-free -disable-llvm-verifier -discard-value-names -main-file-
name UnifiedSource-3a3c4ec0-1.cpp -analyzer-store=region -analyzer-opt-analyze-
nested-blocks -analyzer-checker=core -analyzer-checker=apiModeling -analyzer-
checker=unix -analyzer-checker=deadcode -analyzer-checker=cplusplus -analyzer-
checker=security.insecureAPI.UncheckedReturn -analyzer-
checker=security.insecureAPI.getpw -analyzer-checker=security.insecureAPI.gets -
analyzer-checker=security.insecureAPI.mktemp -analyzer-
checker=security.insecureAPI.mkstemp -analyzer-
checker=security.insecureAPI.vfork -analyzer-
checker=nullability.NullPassedToNonnull -analyzer-
checker=nullability.NullReturnedFromNonnull -analyzer-output plist -w -analyzer-
config-compatibility-mode=true -mrelocation-model pic -pic-level 2 -mthread-
model posix -relaxed-aliasing -fmath-errno -ffp-contract=off -masm-verbose -
mconstructor-aliases -munwind-tables -fuse-init-array -target-cpu x86-64 -dwarf-
column-info -debugger-tuning=gdb -momit-leaf-frame-pointer -resource-dir
/home/pmatos/installs/lib/clang/8.0.1 -D BUILDING_JSCONLY__ -D
BUILDING_JavaScriptCore -D BUILDING_WITH_CMAKE=1 -D HAVE_CONFIG_H=1 -D
JavaScriptCore_EXPORTS -D STATICALLY_LINKED_WITH_WTF -I
DerivedSources/ForwardingHeaders -I . -I ../Source/JavaScriptCore -I
../Source/JavaScriptCore/API -I ../Source/JavaScriptCore/assembler -I
../Source/JavaScriptCore/b3 -I ../Source/JavaScriptCore/b3/air -I
../Source/JavaScriptCore/bindings -I ../Source/JavaScriptCore/builtins -I
../Source/JavaScriptCore/bytecode -I ../Source/JavaScriptCore/bytecompiler -I
../Source/JavaScriptCore/dfg -I ../Source/JavaScriptCore/disassembler -I
../Source/JavaScriptCore/disassembler/ARM64 -I
../Source/JavaScriptCore/disassembler/udis86 -I ../Source/JavaScriptCore/domjit
-I ../Source/JavaScriptCore/ftl -I ../Source/JavaScriptCore/heap -I
../Source/JavaScriptCore/debugger -I ../Source/JavaScriptCore/inspector -I
../Source/JavaScriptCore/inspector/agents -I
../Source/JavaScriptCore/inspector/augmentable -I
../Source/JavaScriptCore/inspector/remote -I
../Source/JavaScriptCore/interpreter -I ../Source/JavaScriptCore/jit -I
../Source/JavaScriptCore/llint -I ../Source/JavaScriptCore/parser -I
../Source/JavaScriptCore/profiler -I ../Source/JavaScriptCore/runtime -I
../Source/JavaScriptCore/tools -I ../Source/JavaScriptCore/wasm -I
../Source/JavaScriptCore/wasm/js -I ../Source/JavaScriptCore/yarr -I
DerivedSources/JavaScriptCore -I DerivedSources/JavaScriptCore/inspector -I
DerivedSources/JavaScriptCore/runtime -I DerivedSources/JavaScriptCore/yarr -I
../Source/bmalloc -I DerivedSources -I ../Source/ThirdParty -D NDEBUG -internal-
isystem /usr/lib/gcc/x86_64-linux-gnu/7.4.0/../../../../include/c++/7.4.0 -
internal-isystem /usr/lib/gcc/x86_64-linux-gnu/7.4.0/../../../../include/x86_64-
linux-gnu/c++/7.4.0 -internal-isystem /usr/lib/gcc/x86_64-linux-
gnu/7.4.0/../../../../include/x86_64-linux-gnu/c++/7.4.0 -internal-isystem
/usr/lib/gcc/x86_64-linux-gnu/7.4.0/../../../../include/c++/7.4.0/backward -
internal-isystem /usr/local/include -internal-isystem
/home/pmatos/installs/lib/clang/8.0.1/include -internal-externc-isystem
/usr/include/x86_64-linux-gnu -internal-externc-isystem /include -internal-
externc-isystem /usr/include -O3 -Wno-expansion-to-defined -Wno-attributes -Wno-
psabi -Wno-noexcept-type -Wno-maybe-uninitialized -std=c++17 -fdeprecated-macro
-fdebug-compilation-dir /home/pmatos/Projects/Igalia/WebKit/WebKitBuild -ferror-
limit 19 -fmessage-length 0 -fno-rtti -fobjc-runtime=gcc -fdiagnostics-show-
option -fcolor-diagnostics -vectorize-loops -vectorize-slp -analyzer-
output=html -analyzer-config crosscheck-with-z3=true -o
/home/pmatos/Projects/Igalia/WebKit/WebKitBuild/build-analysis_z3/scan-build-
2019-05-09-09-46-21-907905-qrljzo0e -x c++
/home/pmatos/Projects/Igalia/WebKit/WebKitBuild/DerivedSources/JavaScriptCore/unified-
sources/UnifiedSource-3a3c4ec0-1.cpp -faddrsig
fatal error: error in backend: Z3 error: rm and float sorts expected

UnifiedSource-3a3c4ec0-1.cpp contains only:
#include "jit/AssemblyHelpers.cpp"
#include "jit/BinarySwitch.cpp"
#include "jit/CCallHelpers.cpp"
#include "jit/CachedRecovery.cpp"
#include "jit/CallFrameShuffleData.cpp"
#include "jit/CallFrameShuffler.cpp"
#include "jit/CallFrameShuffler32_64.cpp"
#include "jit/CallFrameShuffler64.cpp"

If I preprocess this file and rerun the analysis I find no problems anymore.
What further information do you need to debug this?
Quuxplusone commented 5 years ago 
The steps to repro are:
* Grab webkit.
* In top directory:
Tools/Scripts/build-jsc --jsc-only --release
* cd WebKitBuild/Release
* cmake -DCMAKE_BUILD_TYPE=Release -GNinja -DPORT=JSCOnly -
DCMAKE_EXPORT_COMPILE_COMMANDS=ON
* pip install scan-build
* analyze-build --cdb compile_commands.json -o build-analysis -analyzer-config
'crosscheck-with-z3=true'
Quuxplusone commented 5 years ago

We currently don't actively support the experimental Z3 crosscheck, it might be wonky but it's unlikely i'll have time to fix it. I added Mikhail, let's see if he can take a look.

Also you can try to preprocess with -frewrite-includes, this usually preserves the issue much better.

Quuxplusone commented 5 years ago

Hi, I'm happy to have a look at it.

Quuxplusone commented 5 years ago

Paulo, I can't reproduce with the current HEAD of clang...

I think the problem was related to a fix I pushed (82c7651182f65df0) some time ago; it was released part of clang 8.

May I ask you to try again with the current HEAD of clang and report it the problem persists?

Quuxplusone commented 5 years ago 
(In reply to Mikhail from comment #4)
> Paulo, I can't reproduce with the current HEAD of clang...
>
> I think the problem was related to a fix I pushed (82c7651182f65df0) some
> time ago; it was released part of clang 8.
>
> May I ask you to try again with the current HEAD of clang and report it the
> problem persists?

Sure, let me give HEAD of master today a try.
Quuxplusone commented 5 years ago 
(In reply to Mikhail from comment #4)
> Paulo, I can't reproduce with the current HEAD of clang...
>
> I think the problem was related to a fix I pushed (82c7651182f65df0) some
> time ago; it was released part of clang 8.
>
> May I ask you to try again with the current HEAD of clang and report it the
> problem persists?

I can still see the problem with:
# clang --version
clang version 9.0.0 (https://github.com/llvm/llvm-project.git
62889b0ea54b0ee52ef5d09b974bb1565d36472e)
Target: x86_64-unknown-linux-gnu
Thread model: posix
InstalledDir: /root/install/bin
Quuxplusone commented 5 years ago 
# /root/install/bin/clang-9 -cc1 -triple x86_64-unknown-linux-gnu -analyze -
disable-free -disable-llvm-verifier -discard-value-names -main-file-name
UnifiedSource-15db4ad9-5.cpp -analyzer-store=region -analyzer-opt-analyze-
nested-blocks -analyzer-checker=core -analyzer-checker=apiModeling -analyzer-
checker=unix -analyzer-checker=deadcode -analyzer-checker=cplusplus -analyzer-
checker=security.insecureAPI.UncheckedReturn -analyzer-
checker=security.insecureAPI.getpw -analyzer-checker=security.insecureAPI.gets -
analyzer-checker=security.insecureAPI.mktemp -analyzer-
checker=security.insecureAPI.mkstemp -analyzer-
checker=security.insecureAPI.vfork -analyzer-
checker=nullability.NullPassedToNonnull -analyzer-
checker=nullability.NullReturnedFromNonnull -analyzer-output plist -w -analyzer-
config-compatibility-mode=true -mrelocation-model pic -pic-level 2 -mthread-
model posix -relaxed-aliasing -fmath-errno -ffp-contract=off -masm-verbose -
mconstructor-aliases -munwind-tables -fuse-init-array -target-cpu x86-64 -dwarf-
column-info -debugger-tuning=gdb -momit-leaf-frame-pointer -resource-dir
/root/install/lib/clang/9.0.0 -D BUILDING_JSCONLY__ -D BUILDING_JavaScriptCore -
D BUILDING_WITH_CMAKE=1 -D HAVE_CONFIG_H=1 -D JavaScriptCore_EXPORTS -D
STATICALLY_LINKED_WITH_WTF -I DerivedSources/ForwardingHeaders -I . -I
../../Source/JavaScriptCore -I ../../Source/JavaScriptCore/API -I
../../Source/JavaScriptCore/assembler -I ../../Source/JavaScriptCore/b3 -I
../../Source/JavaScriptCore/b3/air -I ../../Source/JavaScriptCore/bindings -I
../../Source/JavaScriptCore/builtins -I ../../Source/JavaScriptCore/bytecode -I
../../Source/JavaScriptCore/bytecompiler -I ../../Source/JavaScriptCore/dfg -I
../../Source/JavaScriptCore/disassembler -I
../../Source/JavaScriptCore/disassembler/ARM64 -I
../../Source/JavaScriptCore/disassembler/udis86 -I
../../Source/JavaScriptCore/domjit -I ../../Source/JavaScriptCore/ftl -I
../../Source/JavaScriptCore/heap -I ../../Source/JavaScriptCore/debugger -I
../../Source/JavaScriptCore/inspector -I
../../Source/JavaScriptCore/inspector/agents -I
../../Source/JavaScriptCore/inspector/augmentable -I
../../Source/JavaScriptCore/inspector/remote -I
../../Source/JavaScriptCore/interpreter -I ../../Source/JavaScriptCore/jit -I
../../Source/JavaScriptCore/llint -I ../../Source/JavaScriptCore/parser -I
../../Source/JavaScriptCore/profiler -I ../../Source/JavaScriptCore/runtime -I
../../Source/JavaScriptCore/tools -I ../../Source/JavaScriptCore/wasm -I
../../Source/JavaScriptCore/wasm/js -I ../../Source/JavaScriptCore/yarr -I
DerivedSources/JavaScriptCore -I DerivedSources/JavaScriptCore/inspector -I
DerivedSources/JavaScriptCore/runtime -I DerivedSources/JavaScriptCore/yarr -I
DerivedSources -I ../../Source/ThirdParty -D NDEBUG -internal-isystem
/usr/lib/gcc/x86_64-linux-gnu/7.4.0/../../../../include/c++/7.4.0 -internal-
isystem /usr/lib/gcc/x86_64-linux-gnu/7.4.0/../../../../include/x86_64-linux-
gnu/c++/7.4.0 -internal-isystem /usr/lib/gcc/x86_64-linux-
gnu/7.4.0/../../../../include/x86_64-linux-gnu/c++/7.4.0 -internal-isystem
/usr/lib/gcc/x86_64-linux-gnu/7.4.0/../../../../include/c++/7.4.0/backward -
internal-isystem /usr/local/include -internal-isystem
/root/install/lib/clang/9.0.0/include -internal-externc-isystem
/usr/include/x86_64-linux-gnu -internal-externc-isystem /include -internal-
externc-isystem /usr/include -O3 -Wno-expansion-to-defined -Wno-attributes -Wno-
psabi -Wno-noexcept-type -Wno-maybe-uninitialized -std=c++1z -fdeprecated-macro
-fdebug-compilation-dir /root/WebKit/WebKitBuild/Release -ferror-limit 19 -
fmessage-length 0 -fno-rtti -fobjc-runtime=gcc -fdiagnostics-show-option -
fcolor-diagnostics -vectorize-loops -vectorize-slp -analyzer-output=html -
analyzer-config crosscheck-with-z3=true -faddrsig -o
/root/WebKit/WebKitBuild/Release/build-analysis/scan-build-2019-06-28-08-32-54-
635388-nNMeVS -x c++
/root/WebKit/WebKitBuild/Release/DerivedSources/JavaScriptCore/unified-sources/UnifiedSource-15db4ad9-5.cpp
fatal error: error in backend: Z3 error: Argument $103 at position 1 does not
match declaration (declare-fun bvule ((_ BitVec 8) (_ BitVec 8)) Bool)

The reason you cannot grab webkit and reproduce this straight away is because
it generates these UnifiedSource files every time anew.
Quuxplusone commented 5 years ago 
Unfortunately again the preprocessed file doesn't break. I preprocess it with -
E -frewrite-includes into UnifiedIncludes.i:
/root/install/bin/clang-9 -cc1 -triple x86_64-unknown-linux-gnu -disable-free -
disable-llvm-verifier -discard-value-names -main-file-name UnifiedSource-
15db4ad9-5.cpp -analyzer-store=region -analyzer-opt-analyze-nested-blocks -
analyzer-checker=core -analyzer-checker=apiModeling -analyzer-checker=unix -
analyzer-checker=deadcode -analyzer-checker=cplusplus -analyzer-
checker=security.insecureAPI.UncheckedReturn -analyzer-
checker=security.insecureAPI.getpw -analyzer-checker=security.insecureAPI.gets -
analyzer-checker=security.insecureAPI.mktemp -analyzer-
checker=security.insecureAPI.mkstemp -analyzer-
checker=security.insecureAPI.vfork -analyzer-
checker=nullability.NullPassedToNonnull -analyzer-
checker=nullability.NullReturnedFromNonnull -analyzer-output plist -w -analyzer-
config-compatibility-mode=true -mrelocation-model pic -pic-level 2 -mthread-
model posix -relaxed-aliasing -fmath-errno -ffp-contract=off -masm-verbose -
mconstructor-aliases -munwind-tables -fuse-init-array -target-cpu x86-64 -dwarf-
column-info -debugger-tuning=gdb -momit-leaf-frame-pointer -resource-dir
/root/install/lib/clang/9.0.0 -D BUILDING_JSCONLY__ -D BUILDING_JavaScriptCore -
D BUILDING_WITH_CMAKE=1 -D HAVE_CONFIG_H=1 -D JavaScriptCore_EXPORTS -D
STATICALLY_LINKED_WITH_WTF -I DerivedSources/ForwardingHeaders -I . -I
../../Source/JavaScriptCore -I ../../Source/JavaScriptCore/API -I
../../Source/JavaScriptCore/assembler -I ../../Source/JavaScriptCore/b3 -I
../../Source/JavaScriptCore/b3/air -I ../../Source/JavaScriptCore/bindings -I
../../Source/JavaScriptCore/builtins -I ../../Source/JavaScriptCore/bytecode -I
../../Source/JavaScriptCore/bytecompiler -I ../../Source/JavaScriptCore/dfg -I
../../Source/JavaScriptCore/disassembler -I
../../Source/JavaScriptCore/disassembler/ARM64 -I
../../Source/JavaScriptCore/disassembler/udis86 -I
../../Source/JavaScriptCore/domjit -I ../../Source/JavaScriptCore/ftl -I
../../Source/JavaScriptCore/heap -I ../../Source/JavaScriptCore/debugger -I
../../Source/JavaScriptCore/inspector -I
../../Source/JavaScriptCore/inspector/agents -I
../../Source/JavaScriptCore/inspector/augmentable -I
../../Source/JavaScriptCore/inspector/remote -I
../../Source/JavaScriptCore/interpreter -I ../../Source/JavaScriptCore/jit -I
../../Source/JavaScriptCore/llint -I ../../Source/JavaScriptCore/parser -I
../../Source/JavaScriptCore/profiler -I ../../Source/JavaScriptCore/runtime -I
../../Source/JavaScriptCore/tools -I ../../Source/JavaScriptCore/wasm -I
../../Source/JavaScriptCore/wasm/js -I ../../Source/JavaScriptCore/yarr -I
DerivedSources/JavaScriptCore -I DerivedSources/JavaScriptCore/inspector -I
DerivedSources/JavaScriptCore/runtime -I DerivedSources/JavaScriptCore/yarr -I
DerivedSources -I ../../Source/ThirdParty -D NDEBUG -internal-isystem
/usr/lib/gcc/x86_64-linux-gnu/7.4.0/../../../../include/c++/7.4.0 -internal-
isystem /usr/lib/gcc/x86_64-linux-gnu/7.4.0/../../../../include/x86_64-linux-
gnu/c++/7.4.0 -internal-isystem /usr/lib/gcc/x86_64-linux-
gnu/7.4.0/../../../../include/x86_64-linux-gnu/c++/7.4.0 -internal-isystem
/usr/lib/gcc/x86_64-linux-gnu/7.4.0/../../../../include/c++/7.4.0/backward -
internal-isystem /usr/local/include -internal-isystem
/root/install/lib/clang/9.0.0/include -internal-externc-isystem
/usr/include/x86_64-linux-gnu -internal-externc-isystem /include -internal-
externc-isystem /usr/include -O3 -Wno-expansion-to-defined -Wno-attributes -Wno-
psabi -Wno-noexcept-type -Wno-maybe-uninitialized -std=c++1z -fdeprecated-macro
-fdebug-compilation-dir /root/WebKit/WebKitBuild/Release -ferror-limit 19 -
fmessage-length 0 -fno-rtti -fobjc-runtime=gcc -fdiagnostics-show-option -
fcolor-diagnostics -vectorize-loops -vectorize-slp -faddrsig -o
/root/WebKit/WebKitBuild/Release/UnifiedIncludes.i -frewrite-includes -E -x c++
/root/WebKit/WebKitBuild/Release/DerivedSources/JavaScriptCore/unified-sources/UnifiedSource-15db4ad9-5.cpp

Then I run the analysis on the UnifiedIncludes.i:
/root/install/bin/clang-9 -cc1 -triple x86_64-unknown-linux-gnu -analyze -
disable-free -disable-llvm-verifier -discard-value-names -main-file-name
UnifiedSource-15db4ad9-5.cpp -analyzer-store=region -analyzer-opt-analyze-
nested-blocks -analyzer-checker=core -analyzer-checker=apiModeling -analyzer-
checker=unix -analyzer-checker=deadcode -analyzer-checker=cplusplus -analyzer-
checker=security.insecureAPI.UncheckedReturn -analyzer-
checker=security.insecureAPI.getpw -analyzer-checker=security.insecureAPI.gets -
analyzer-checker=security.insecureAPI.mktemp -analyzer-
checker=security.insecureAPI.mkstemp -analyzer-
checker=security.insecureAPI.vfork -analyzer-
checker=nullability.NullPassedToNonnull -analyzer-
checker=nullability.NullReturnedFromNonnull -analyzer-output plist -w -analyzer-
config-compatibility-mode=true -mrelocation-model pic -pic-level 2 -mthread-
model posix -relaxed-aliasing -fmath-errno -ffp-contract=off -masm-verbose -
mconstructor-aliases -munwind-tables -fuse-init-array -target-cpu x86-64 -dwarf-
column-info -debugger-tuning=gdb -momit-leaf-frame-pointer -resource-dir
/root/install/lib/clang/9.0.0 -D BUILDING_JSCONLY__ -D BUILDING_JavaScriptCore -
D BUILDING_WITH_CMAKE=1 -D HAVE_CONFIG_H=1 -D JavaScriptCore_EXPORTS -D
STATICALLY_LINKED_WITH_WTF -I DerivedSources/ForwardingHeaders -I . -I
../../Source/JavaScriptCore -I ../../Source/JavaScriptCore/API -I
../../Source/JavaScriptCore/assembler -I ../../Source/JavaScriptCore/b3 -I
../../Source/JavaScriptCore/b3/air -I ../../Source/JavaScriptCore/bindings -I
../../Source/JavaScriptCore/builtins -I ../../Source/JavaScriptCore/bytecode -I
../../Source/JavaScriptCore/bytecompiler -I ../../Source/JavaScriptCore/dfg -I
../../Source/JavaScriptCore/disassembler -I
../../Source/JavaScriptCore/disassembler/ARM64 -I
../../Source/JavaScriptCore/disassembler/udis86 -I
../../Source/JavaScriptCore/domjit -I ../../Source/JavaScriptCore/ftl -I
../../Source/JavaScriptCore/heap -I ../../Source/JavaScriptCore/debugger -I
../../Source/JavaScriptCore/inspector -I
../../Source/JavaScriptCore/inspector/agents -I
../../Source/JavaScriptCore/inspector/augmentable -I
../../Source/JavaScriptCore/inspector/remote -I
../../Source/JavaScriptCore/interpreter -I ../../Source/JavaScriptCore/jit -I
../../Source/JavaScriptCore/llint -I ../../Source/JavaScriptCore/parser -I
../../Source/JavaScriptCore/profiler -I ../../Source/JavaScriptCore/runtime -I
../../Source/JavaScriptCore/tools -I ../../Source/JavaScriptCore/wasm -I
../../Source/JavaScriptCore/wasm/js -I ../../Source/JavaScriptCore/yarr -I
DerivedSources/JavaScriptCore -I DerivedSources/JavaScriptCore/inspector -I
DerivedSources/JavaScriptCore/runtime -I DerivedSources/JavaScriptCore/yarr -I
DerivedSources -I ../../Source/ThirdParty -D NDEBUG -internal-isystem
/usr/lib/gcc/x86_64-linux-gnu/7.4.0/../../../../include/c++/7.4.0 -internal-
isystem /usr/lib/gcc/x86_64-linux-gnu/7.4.0/../../../../include/x86_64-linux-
gnu/c++/7.4.0 -internal-isystem /usr/lib/gcc/x86_64-linux-
gnu/7.4.0/../../../../include/x86_64-linux-gnu/c++/7.4.0 -internal-isystem
/usr/lib/gcc/x86_64-linux-gnu/7.4.0/../../../../include/c++/7.4.0/backward -
internal-isystem /usr/local/include -internal-isystem
/root/install/lib/clang/9.0.0/include -internal-externc-isystem
/usr/include/x86_64-linux-gnu -internal-externc-isystem /include -internal-
externc-isystem /usr/include -O3 -Wno-expansion-to-defined -Wno-attributes -Wno-
psabi -Wno-noexcept-type -Wno-maybe-uninitialized -std=c++1z -fdeprecated-macro
-fdebug-compilation-dir /root/WebKit/WebKitBuild/Release -ferror-limit 19 -
fmessage-length 0 -fno-rtti -fobjc-runtime=gcc -fdiagnostics-show-option -
fcolor-diagnostics -vectorize-loops -vectorize-slp -analyzer-output=html -
analyzer-config crosscheck-with-z3=true -faddrsig -o
/root/WebKit/WebKitBuild/Release/build-analysis/scan-build-2019-06-28-08-32-54-
635388-nNMeVS -x c++ /root/WebKit/WebKitBuild/Release/UnifiedIncludes.i

This works without a hitch. Is there a way to request debug information from
Z3? I assume that you are calling libz3 functions. Can I trace those? Maybe
with that trace we can understand what's bugging z3.
Quuxplusone commented 5 years ago

Alternatively I can also create a script that triggers the bug inside a docker container if you prefer to look at it yourselves.

Quuxplusone commented 5 years ago

Attached 0001-Hack-to-avoid-crash-in-WebKit.patch (1967 bytes, text/plain): Hack to fix the second crash

Quuxplusone commented 5 years ago

Thanks for looking at this. I will give you patch a go.

Quuxplusone commented 5 years ago

Mikhail. Your patch worked. Thanks.

Quuxplusone commented 5 years ago

I just sent an email to the mailing list asking for some guidance:

http://lists.llvm.org/pipermail/cfe-dev/2019-June/062744.html

Quuxplusone commented 5 years ago

@Mikhail, what's the status of this?

Quuxplusone commented 4 years ago

Is there a reason this didn't make it upstream?

Quuxplusone commented 4 years ago

I was hoping to find time to fix the CSA instead of messing with the clang internals :/

The issue is that the CSA is dropping the casts. There was a PR with a fix submitted a few years ago but it seems to be abandoned: https://reviews.llvm.org/D28955. I'm not sure if it fixes the issue you reported though.

Artem, do you have any plan to have another look at the support for truncation/extension in the CSA?