<html>
<head>
<base href="https://bugs.llvm.org/">
</head>
<body><table border="1" cellspacing="0" cellpadding="8">
<tr>
<th>Bug ID</th>
<td><a class="bz_bug_link
bz_status_NEW "
title="NEW - z3 fatal error while analyzing webkit"
href="https://bugs.llvm.org/show_bug.cgi?id=41809">41809</a>
</td>
</tr>
<tr>
<th>Summary</th>
<td>z3 fatal error while analyzing webkit
</td>
</tr>
<tr>
<th>Product</th>
<td>clang
</td>
</tr>
<tr>
<th>Version</th>
<td>8.0
</td>
</tr>
<tr>
<th>Hardware</th>
<td>PC
</td>
</tr>
<tr>
<th>OS</th>
<td>Linux
</td>
</tr>
<tr>
<th>Status</th>
<td>NEW
</td>
</tr>
<tr>
<th>Severity</th>
<td>enhancement
</td>
</tr>
<tr>
<th>Priority</th>
<td>P
</td>
</tr>
<tr>
<th>Component</th>
<td>C++
</td>
</tr>
<tr>
<th>Assignee</th>
<td>unassignedclangbugs@nondot.org
</td>
</tr>
<tr>
<th>Reporter</th>
<td>pmatos@linki.tools
</td>
</tr>
<tr>
<th>CC</th>
<td>blitzrakete@gmail.com, dgregor@apple.com, erik.pilkington@gmail.com, llvm-bugs@lists.llvm.org, richard-llvm@metafoo.co.uk
</td>
</tr></table>
<p>
<div>
<pre>During a WebKit (<a href="https://webkit.org/">https://webkit.org/</a>) 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?</pre>
</div>
</p>
<hr>
<span>You are receiving this mail because:</span>
<ul>
<li>You are on the CC list for the bug.</li>
</ul>
</body>
</html>