eurecom-s3 / symcc

SymCC: efficient compiler-based symbolic execution
http://www.s3.eurecom.fr/tools/symbolic_execution/symcc.html
GNU General Public License v3.0
776 stars 135 forks source link

SymCC doesn't handle SSE instructions properly and crashes in debug builds (UNREACHABLE executed at ../compiler/Symbolizer.cpp:880! when building OpenJPEG) #10

Open thetheodor opened 4 years ago

thetheodor commented 4 years ago

Hi, I'm trying to build OpenJPEG but symcc (clang 10.0.1) is crushing. I've built the master branch of symcc and 1f1e9682 of OpenJPEG with:

CC=~/symcc/build/symcc CXX=~/symcc/build/sym++ SYMCC_NO_SYMBOLIC_INPUT=1 SYMCC_LIBCXX_PATH=/usr/include/c++/v1 cmake .. -DCMAKE_BUILD_TYPE=Release -DBUILD_THIRDPARTY=ON

However, building src/lib/openjp2/CMakeFiles/openjp2.dir/dwt.c.o fails with:

/home/theo/symcc/build/symcc -Dopenjp2_EXPORTS -Isrc/lib/openjp2 -O3 -DNDEBUG -fPIC -MD -MT src/lib/openjp2/CMakeFiles/openjp2.dir/dwt.c.o -MF src/lib/openjp2/CMakeFiles/openjp2.dir/dwt.c.o.d -o src/lib/openjp2/CMakeFiles/openjp2.dir/dwt.c.o -c ../src/lib/openjp2/dwt.c
Symbolizer module init
Symbolizing function opj_dwt_encode
Symbolizing function opj_dwt_encode_procedure
Symbolizing function opj_dwt_encode_1
Symbolizing function opj_dwt_decode
Symbolizing function opj_dwt_decode_1
Symbolizing function opj_dwt_getgain
Symbolizing function opj_dwt_getnorm
Symbolizing function opj_dwt_encode_real
Symbolizing function opj_dwt_encode_1_real
Symbolizing function opj_dwt_getgain_real
Symbolizing function opj_dwt_getnorm_real
Symbolizing function opj_dwt_calc_explicit_stepsizes
Warning: unhandled LLVM intrinsic llvm.floor.f64
Symbolizing function opj_dwt_decode_real
Symbolizing function opj_v4dwt_interleave_h
Symbolizing function opj_v4dwt_decode
Unhandled type for constant expression
UNREACHABLE executed at ../compiler/Symbolizer.cpp:880!
Stack dump:
0.  Program arguments: /usr/bin/clang -Xclang -load -Xclang /home/theo/symcc/build/libSymbolize.so -Dopenjp2_EXPORTS -Isrc/lib/openjp2 -O3 -DNDEBUG -fPIC -MD -MT src/lib/openjp2/CMakeFiles/openjp2.dir/dwt.c.o -MF src/lib/openjp2/CMakeFiles/openjp2.dir/dwt.c.o.d -o src/lib/openjp2/CMakeFiles/openjp2.dir/dwt.c.o -c ../src/lib/openjp2/dwt.c -L/home/theo/symcc/build/SymRuntime-prefix/src/SymRuntime-build -lSymRuntime -Wl,-rpath,/home/theo/symcc/build/SymRuntime-prefix/src/SymRuntime-build -Qunused-arguments
1.  <eof> parser at end of file
2.  Per-module optimization passes
3.  Running pass 'Function Pass Manager' on module '../src/lib/openjp2/dwt.c'.
4.  Running pass 'Symbolization Pass' on function '@opj_v4dwt_decode'
 #0 0x00007f98da3efeeb llvm::sys::PrintStackTrace(llvm::raw_ostream&) (/usr/bin/../lib/libLLVM-10.so+0x9e9eeb)
 #1 0x00007f98da3eda44 llvm::sys::RunSignalHandlers() (/usr/bin/../lib/libLLVM-10.so+0x9e7a44)
 #2 0x00007f98da3104c9 (/usr/bin/../lib/libLLVM-10.so+0x90a4c9)
 #3 0x00007f98d969e3e0 __restore_rt (/usr/bin/../lib/libc.so.6+0x3c3e0)
 #4 0x00007f98d969e355 raise (/usr/bin/../lib/libc.so.6+0x3c355)
 #5 0x00007f98d9687853 abort (/usr/bin/../lib/libc.so.6+0x25853)
 #6 0x00007f98da31fb90 LLVMInstallFatalErrorHandler (/usr/bin/../lib/libLLVM-10.so+0x919b90)
 #7 0x00007f98d74f832b Symbolizer::createValueExpression(llvm::Value*, llvm::IRBuilder<llvm::ConstantFolder, llvm::IRBuilderDefaultInserter>&) (/home/theo/symcc/build/libSymbolize.so+0x5a32b)
 #8 0x00007f98d74f278b Symbolizer::shortCircuitExpressionUses() (/home/theo/symcc/build/libSymbolize.so+0x5478b)
 #9 0x00007f98d750d4d3 SymbolizePass::runOnFunction(llvm::Function&) (/home/theo/symcc/build/libSymbolize.so+0x6f4d3)
#10 0x00007f98da5215d8 llvm::FPPassManager::runOnFunction(llvm::Function&) (/usr/bin/../lib/libLLVM-10.so+0xb1b5d8)
#11 0x00007f98da522bdd llvm::FPPassManager::runOnModule(llvm::Module&) (/usr/bin/../lib/libLLVM-10.so+0xb1cbdd)
#12 0x00007f98da522f70 llvm::legacy::PassManagerImpl::run(llvm::Module&) (/usr/bin/../lib/libLLVM-10.so+0xb1cf70)
#13 0x00007f98e0424a25 clang::EmitBackendOutput(clang::DiagnosticsEngine&, clang::HeaderSearchOptions const&, clang::CodeGenOptions const&, clang::TargetOptions const&, clang::LangOptions const&, llvm::DataLayout const&, llvm::Module*, clang::BackendAction, std::unique_ptr<llvm::raw_pwrite_stream, std::default_delete<llvm::raw_pwrite_stream> >) (/usr/bin/../lib/libclang-cpp.so.10+0x1603a25)
#14 0x00007f98e076f67b (/usr/bin/../lib/libclang-cpp.so.10+0x194e67b)
#15 0x00007f98df624ad9 clang::ParseAST(clang::Sema&, bool, bool) (/usr/bin/../lib/libclang-cpp.so.10+0x803ad9)
#16 0x00007f98e0eb20a9 clang::FrontendAction::Execute() (/usr/bin/../lib/libclang-cpp.so.10+0x20910a9)
#17 0x00007f98e0e66a94 clang::CompilerInstance::ExecuteAction(clang::FrontendAction&) (/usr/bin/../lib/libclang-cpp.so.10+0x2045a94)
#18 0x00007f98e0f36832 clang::ExecuteCompilerInvocation(clang::CompilerInstance*) (/usr/bin/../lib/libclang-cpp.so.10+0x2115832)
#19 0x0000561e59f477ed cc1_main(llvm::ArrayRef<char const*>, char const*, void*) (/usr/bin/clang+0x127ed)
#20 0x0000561e59f44ffc (/usr/bin/clang+0xfffc)
#21 0x00007f98e0b33165 (/usr/bin/../lib/libclang-cpp.so.10+0x1d12165)
#22 0x00007f98da3105e3 llvm::CrashRecoveryContext::RunSafely(llvm::function_ref<void ()>) (/usr/bin/../lib/libLLVM-10.so+0x90a5e3)
#23 0x00007f98e0b33fae (/usr/bin/../lib/libclang-cpp.so.10+0x1d12fae)
#24 0x00007f98e0b09b68 clang::driver::Compilation::ExecuteCommand(clang::driver::Command const&, clang::driver::Command const*&) const (/usr/bin/../lib/libclang-cpp.so.10+0x1ce8b68)
#25 0x00007f98e0b0a45a clang::driver::Compilation::ExecuteJobs(clang::driver::JobList const&, llvm::SmallVectorImpl<std::pair<int, clang::driver::Command const*> >&) const (/usr/bin/../lib/libclang-cpp.so.10+0x1ce945a)
#26 0x00007f98e0b15ebc clang::driver::Driver::ExecuteCompilation(clang::driver::Compilation&, llvm::SmallVectorImpl<std::pair<int, clang::driver::Command const*> >&) (/usr/bin/../lib/libclang-cpp.so.10+0x1cf4ebc)
#27 0x0000561e59f42d09 main (/usr/bin/clang+0xdd09)
#28 0x00007f98d9689002 __libc_start_main (/usr/bin/../lib/libc.so.6+0x27002)
#29 0x0000561e59f4496e _start (/usr/bin/clang+0xf96e)
clang-10: error: clang frontend command failed due to signal (use -v to see invocation)
clang version 10.0.1
Target: x86_64-pc-linux-gnu
Thread model: posix
InstalledDir: /usr/bin
clang-10: note: diagnostic msg: PLEASE submit a bug report to  and include the crash backtrace, preprocessed source, and associated run script.
clang-10: note: diagnostic msg:

Am I doing something wrong?

Thanks

sebastianpoeplau commented 4 years ago

Hi @ttheodor,

There's no error on your side, and I can reproduce the problem. The TL;DR is that OpenJPEG seems to automatically use SSE instructions when they're available, resulting in code that SymCC doesn't understand. Building SymCC in release mode and using it to compile OpenJPEG avoids the error, but only by chance.

The longer version:

The assertion error Unhandled type for constant expression means that SymCC encounters a constant in the code that it doesn't understand. The function in question, opj_v4dwt_decode, contains conditionally compiled SSE code (https://github.com/uclouvain/openjpeg/blob/cbee7891a0ee664dd83ca09553d2e30da716a883/src/lib/openjp2/dwt.c#L2460). This is the cause of the error; to confirm, I ran the failing compiler command with regular clang, asking it to produce LLVM IR output:

$ clang -Dopenjp2_EXPORTS -Isrc/lib/openjp2 -O3 -DNDEBUG -fPIC -MD -MT src/lib/openjp2/CMakeFiles/openjp2.dir/dwt.c.o -MF src/lib/openjp2/CMakeFiles/openjp2.dir/dwt.c.o.d -S -emit-llvm -o- ../src/lib/openjp2/dwt.c

The output will be the LLVM representation of the C code; the function opj_v4dwt_decode indeed contains vector instructions:

define internal fastcc void @opj_v4dwt_decode(%struct.v4dwt_local* noalias nocapture readonly %0) unnamed_addr #8 {
...
  %35 = phi <4 x float>* [ %47, %33 ], [ %30, %21 ]
  %36 = load <4 x float>, <4 x float>* %35, align 16, !tbaa !127
  %37 = fmul <4 x float> %36, <float 0x3FF3AECB00000000, float 0x3FF3AECB00000000, float 0x3FF3AECB00000000, float 0x3FF3AECB00000000>
...

SymCC should fail when encountering those because we haven't implemented symbolic handling for them. (It's straight-forward and would be nice to have, but so far I haven't had the time.) What I didn't realize is that llvm_unreachable, the function that throws the error, doesn't abort in release builds. So a release version of SymCC would happily accept vector constants, returning some undefined value as the corresponding expression. However, executing the resulting OpenJPEG programs works just fine! The reason is, I think, that the operations performed on those particular vectors are floating-point arithmetic, which the QSYM backend always concretizes. Therefore, the nonsensical expression doesn't cause any harm...

Now, how should we fix this?

thetheodor commented 4 years ago

Thanks for the reply. Using a release version of SymCC seems to work.

xupeng1231 commented 2 years ago

@thetheodor How to build SymCC in release mode? Thanks.

thetheodor commented 2 years ago

@xupeng1231 it's been some time since I played with SymCC so I don't really remember how. My first guess would be to use -DCMAKE_BUILD_TYPE=Release when running cmake.