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
791 stars 139 forks source link

Missing support for arithmetic on booleans and vector types #171

Open exatoa opened 7 months ago

exatoa commented 7 months ago

Hi,

C project with decreasing boolean variables

I'm facing an issue with compiling some code with SymCC. When a code tries to decrease a boolean variable, an error comes. This does not occur when I compile with pure clang. Please take a look at the example source code and error messages below. The code would not be used often in practice, but it is generated by a mutataion analysis tool.

Example code:

#include<stdio.h>
#include<stdbool.h>
int main()
{
        bool var=true;
        var--;
        return 0;
}

Error message:

Can't handle Boolean operator   %11 = add i1 %10, true
double free or corruption (out)
PLEASE submit a bug report to https://github.com/llvm/llvm-project/issues/ and include the crash backtrace, preprocessed source, and associated run script.
Stack dump:
0.      Program arguments: /usr/lib/llvm-14/bin/clang -cc1 -triple x86_64-pc-linux-gnu -emit-obj -mrelax-all --mrelax-relocations -disable-free -clear-ast-before-backend -disable-llvm-verifier -discard-value-names -main-file-name test.c -mrelocation-model pic -pic-level 2 -pic-is-pie -mframe-pointer=all -fmath-errno -ffp-contract=on -fno-rounding-math -mconstructor-aliases -funwind-tables=2 -target-cpu x86-64 -tune-cpu generic -mllvm -treat-scalable-fixed-error-as-warning -debugger-tuning=gdb -fcoverage-compilation-dir=/vagrant/case_studies/S5/repos -resource-dir /usr/lib/llvm-14/lib/clang/14.0.0 -internal-isystem /usr/lib/llvm-14/lib/clang/14.0.0/include -internal-isystem /usr/local/include -internal-isystem /usr/lib/gcc/x86_64-linux-gnu/11/../../../../x86_64-linux-gnu/include -internal-externc-isystem /usr/include/x86_64-linux-gnu -internal-externc-isystem /include -internal-externc-isystem /usr/include -fdebug-compilation-dir=/vagrant/case_studies/S5/repos -ferror-limit 19 -fgnuc-version=4.2.1 -fcolor-diagnostics -fpass-plugin=/opt/symcc/bin/libSymbolize.so -faddrsig -D__GCC_HAVE_DWARF2_CFI_ASM=1 -o /tmp/test-879f50.o -x c test.c
1.      <eof> parser at end of file
2.      Optimizer
 #0 0x00007efe8c37ad01 llvm::sys::PrintStackTrace(llvm::raw_ostream&, int) (/lib/x86_64-linux-gnu/libLLVM-14.so.1+0xe3fd01)
 #1 0x00007efe8c378a3e llvm::sys::RunSignalHandlers() (/lib/x86_64-linux-gnu/libLLVM-14.so.1+0xe3da3e)
 #2 0x00007efe8c37b236 (/lib/x86_64-linux-gnu/libLLVM-14.so.1+0xe40236)
 #3 0x00007efe8b01f520 (/lib/x86_64-linux-gnu/libc.so.6+0x42520)
 #4 0x00007efe8b0739fc __pthread_kill_implementation ./nptl/./nptl/pthread_kill.c:44:76
 #5 0x00007efe8b0739fc __pthread_kill_internal ./nptl/./nptl/pthread_kill.c:78:10
 #6 0x00007efe8b0739fc pthread_kill ./nptl/./nptl/pthread_kill.c:89:10
 #7 0x00007efe8b01f476 gsignal ./signal/../sysdeps/posix/raise.c:27:6
 #8 0x00007efe8b0057f3 abort ./stdlib/./stdlib/abort.c:81:7
 #9 0x00007efe8b066676 __libc_message ./libio/../sysdeps/posix/libc_fatal.c:155:5
#10 0x00007efe8b07dcfc ./malloc/./malloc/malloc.c:5668:3
#11 0x00007efe8b07fe70 _int_free ./malloc/./malloc/malloc.c:4591:7
#12 0x00007efe8b082453 __libc_free ./malloc/./malloc/malloc.c:3394:3
#13 0x00007efe88e72d01 Symbolizer::visitBinaryOperator(llvm::BinaryOperator&) /opt/symcc/src/compiler/Symbolizer.cpp:423:1
#14 0x00007efe88e791cb (anonymous namespace)::instrumentFunction(llvm::Function&) /opt/symcc/src/compiler/Pass.cpp:196:24
#15 0x00007efe88e79651 llvm::SmallPtrSet<void*, 2u>::SmallPtrSet() /usr/include/llvm-14/llvm/ADT/SmallPtrSet.h:464:25
#16 0x00007efe88e79651 llvm::PreservedAnalyses::PreservedAnalyses() /usr/include/llvm-14/llvm/IR/PassManager.h:152:7
#17 0x00007efe88e79651 llvm::PreservedAnalyses::none() /usr/include/llvm-14/llvm/IR/PassManager.h:155:62
#18 0x00007efe88e79651 SymbolizePass::run(llvm::Function&, llvm::AnalysisManager<llvm::Function>&) /opt/symcc/src/compiler/Pass.cpp:223:57
#19 0x00007efe88e7cb36 llvm::detail::PassModel<llvm::Function, SymbolizePass, llvm::PreservedAnalyses, llvm::AnalysisManager<llvm::Function> >::run(llvm::Function&, llvm::AnalysisManager<llvm::Function>&) /usr/include/llvm-14/llvm/IR/PassManagerInternal.h:89:3
#20 0x00007efe8c4e9a0e llvm::PassManager<llvm::Function, llvm::AnalysisManager<llvm::Function> >::run(llvm::Function&, llvm::AnalysisManager<llvm::Function>&) (/lib/x86_64-linux-gnu/libLLVM-14.so.1+0xfaea0e)
#21 0x00007efe8e0d424d (/lib/x86_64-linux-gnu/libLLVM-14.so.1+0x2b9924d)
#22 0x00007efe8c4ed9d1 llvm::ModuleToFunctionPassAdaptor::run(llvm::Module&, llvm::AnalysisManager<llvm::Module>&) (/lib/x86_64-linux-gnu/libLLVM-14.so.1+0xfb29d1)
#23 0x00007efe8e0d407d (/lib/x86_64-linux-gnu/libLLVM-14.so.1+0x2b9907d)
#24 0x00007efe8c4e860e llvm::PassManager<llvm::Module, llvm::AnalysisManager<llvm::Module> >::run(llvm::Module&, llvm::AnalysisManager<llvm::Module>&) (/lib/x86_64-linux-gnu/libLLVM-14.so.1+0xfad60e)
#25 0x00007efe9366fb9b (/lib/x86_64-linux-gnu/libclang-cpp.so.14+0x1862b9b)
#26 0x00007efe93663a52 clang::EmitBackendOutput(clang::DiagnosticsEngine&, clang::HeaderSearchOptions const&, clang::CodeGenOptions const&, clang::TargetOptions const&, clang::LangOptions const&, llvm::StringRef, llvm::Module*, clang::BackendAction, std::unique_ptr<llvm::raw_pwrite_stream, std::default_delete<llvm::raw_pwrite_stream> >) (/lib/x86_64-linux-gnu/libclang-cpp.so.14+0x1856a52)
#27 0x00007efe93989855 (/lib/x86_64-linux-gnu/libclang-cpp.so.14+0x1b7c855)
#28 0x00007efe92811824 clang::ParseAST(clang::Sema&, bool, bool) (/lib/x86_64-linux-gnu/libclang-cpp.so.14+0xa04824)
#29 0x00007efe93985b71 clang::CodeGenAction::ExecuteAction() (/lib/x86_64-linux-gnu/libclang-cpp.so.14+0x1b78b71)
#30 0x00007efe94321b57 clang::FrontendAction::Execute() (/lib/x86_64-linux-gnu/libclang-cpp.so.14+0x2514b57)
#31 0x00007efe942793a6 clang::CompilerInstance::ExecuteAction(clang::FrontendAction&) (/lib/x86_64-linux-gnu/libclang-cpp.so.14+0x246c3a6)
#32 0x00007efe9439b45b clang::ExecuteCompilerInvocation(clang::CompilerInstance*) (/lib/x86_64-linux-gnu/libclang-cpp.so.14+0x258e45b)
#33 0x000000000041328b cc1_main(llvm::ArrayRef<char const*>, char const*, void*) (/usr/lib/llvm-14/bin/clang+0x41328b)
#34 0x00000000004114bc (/usr/lib/llvm-14/bin/clang+0x4114bc)
#35 0x0000000000411307 main (/usr/lib/llvm-14/bin/clang+0x411307)
#36 0x00007efe8b006d90 __libc_start_call_main ./csu/../sysdeps/nptl/libc_start_call_main.h:58:16
#37 0x00007efe8b006e40 call_init ./csu/../csu/libc-start.c:128:20
#38 0x00007efe8b006e40 __libc_start_main ./csu/../csu/libc-start.c:379:5
#39 0x000000000040e3b5 _start (/usr/lib/llvm-14/bin/clang+0x40e3b5)
clang: error: unable to execute command: Aborted (core dumped)
clang: error: clang frontend command failed due to signal (use -v to see invocation)
Ubuntu clang version 14.0.0-1ubuntu1.1
Target: x86_64-pc-linux-gnu
Thread model: posix
InstalledDir: /usr/lib/llvm-14/bin
clang: note: diagnostic msg: 
********************

PLEASE ATTACH THE FOLLOWING FILES TO THE BUG REPORT:
Preprocessed source(s) and associated run script(s) are located at:
clang: note: diagnostic msg: /tmp/test-8a5883.c
clang: note: diagnostic msg: /tmp/test-8a5883.sh
clang: note: diagnostic msg: 

********************

C++ project

Another error happens when I compile a C++ project. Compiling with Clang has no problem, but with SymCC, it has a compile error. I used regular standard library as below:

export SYMCC_REGULAR_LIBCXX=yes
export CC=/opt/symcc/bin/symcc
export CXX=/opt/symcc/bin/sym++
cmake -DLIBS=/opt/lib . 
make

But It has no specific error message, and I cannot share the code, unfortunately. The project code does not contain the above issue code, but it shows...the following error message:

Warning: unknown instruction   %51 = insertelement <4 x double> undef, double %50, i32 0; the result will be concretized
Warning: unknown instruction   %56 = insertelement <4 x double> %51, double %55, i32 1; the result will be concretized
Warning: unknown instruction   %61 = insertelement <4 x double> %56, double %60, i32 2; the result will be concretized
Warning: unknown instruction   %66 = insertelement <4 x double> %61, double %65, i32 3; the result will be concretized
Warning: unknown instruction   %69 = insertelement <8 x i32> undef, i32 %68, i32 0; the result will be concretized
Warning: unknown instruction   %73 = insertelement <8 x i32> %69, i32 %72, i32 1; the result will be concretized
Warning: unknown instruction   %77 = insertelement <8 x i32> %73, i32 %76, i32 2; the result will be concretized
Warning: unknown instruction   %81 = insertelement <8 x i32> %77, i32 %80, i32 3; the result will be concretized
Warning: unknown instruction   %85 = insertelement <8 x i32> %81, i32 %84, i32 4; the result will be concretized
Warning: unknown instruction   %89 = insertelement <8 x i32> %85, i32 %88, i32 5; the result will be concretized
Warning: unknown instruction   %93 = insertelement <8 x i32> %89, i32 %92, i32 6; the result will be concretized
Warning: unknown instruction   %97 = insertelement <8 x i32> %93, i32 %96, i32 7; the result will be concretized
PLEASE submit a bug report to https://github.com/llvm/llvm-project/issues/ and include the crash backtrace, preprocessed source, and associated run script.
Stack dump:
0.      Program arguments: /usr/lib/llvm-14/bin/clang++ -fpass-plugin=/opt/symcc/bin/libSymbolize.so ... -mavx2 -mfma -fopenmp=libomp -std=c++14 ... -o CMakeFiles/source.o -c source.cpp -L/opt/symcc/bin/SymRuntime-prefix/src/SymRuntime-build -lSymRuntime -Wl,-rpath,/opt/symcc/bin/SymRuntime-prefix/src/SymRuntime-build -Qunused-arguments
1.      <eof> parser at end of file
2.      Optimizer
 #0 0x00007f99a5c70d01 llvm::sys::PrintStackTrace(llvm::raw_ostream&, int) (/lib/x86_64-linux-gnu/libLLVM-14.so.1+0xe3fd01)
 #1 0x00007f99a5c6ea3e llvm::sys::RunSignalHandlers() (/lib/x86_64-linux-gnu/libLLVM-14.so.1+0xe3da3e)
 #2 0x00007f99a5c700ab llvm::sys::CleanupOnSignal(unsigned long) (/lib/x86_64-linux-gnu/libLLVM-14.so.1+0xe3f0ab)
 #3 0x00007f99a5b9cdff (/lib/x86_64-linux-gnu/libLLVM-14.so.1+0xd6bdff)
 #4 0x00007f99a4915520 (/lib/x86_64-linux-gnu/libc.so.6+0x42520)
 #5 0x00007f99a5e00b2b llvm::Value::setNameImpl(llvm::Twine const&) (/lib/x86_64-linux-gnu/libLLVM-14.so.1+0xfcfb2b)
 #6 0x00007f99a5e00f29 llvm::Value::setName(llvm::Twine const&) (/lib/x86_64-linux-gnu/libLLVM-14.so.1+0xfcff29)
 #7 0x00007f99a24e2f79 llvm::ExtractValueInst* llvm::IRBuilderBase::Insert<llvm::ExtractValueInst>(llvm::ExtractValueInst*, llvm::Twine const&) const /usr/include/llvm-14/llvm/IR/IRBuilder.h:149:5
 #8 0x00007f99a24e2f79 llvm::IRBuilderBase::CreateExtractValue(llvm::Value*, llvm::ArrayRef<unsigned int>, llvm::Twine const&) /usr/include/llvm-14/llvm/IR/IRBuilder.h:2372:18
 #9 0x00007f99a24d66a2 Symbolizer::createValueExpression(llvm::Value*, llvm::IRBuilder<llvm::ConstantFolder, llvm::IRBuilderDefaultInserter>&) /opt/symcc/src/compiler/Symbolizer.cpp:1030:52
#10 0x00007f99a24d789e Symbolizer::shortCircuitExpressionUses() /opt/symcc/src/compiler/Symbolizer.cpp:147:32
#11 0x00007f99a24e61e4 (anonymous namespace)::instrumentFunction(llvm::Function&) /opt/symcc/src/compiler/Pass.cpp:190:39
#12 0x00007f99a24e6651 llvm::SmallPtrSet<void*, 2u>::SmallPtrSet() /usr/include/llvm-14/llvm/ADT/SmallPtrSet.h:464:25
#13 0x00007f99a24e6651 llvm::PreservedAnalyses::PreservedAnalyses() /usr/include/llvm-14/llvm/IR/PassManager.h:152:7
#14 0x00007f99a24e6651 llvm::PreservedAnalyses::none() /usr/include/llvm-14/llvm/IR/PassManager.h:155:62
#15 0x00007f99a24e6651 SymbolizePass::run(llvm::Function&, llvm::AnalysisManager<llvm::Function>&) /opt/symcc/src/compiler/Pass.cpp:223:57
#16 0x00007f99a24e9b36 llvm::detail::PassModel<llvm::Function, SymbolizePass, llvm::PreservedAnalyses, llvm::AnalysisManager<llvm::Function> >::run(llvm::Function&, llvm::AnalysisManager<llvm::Function>&) /usr/include/llvm-14/llvm/IR/PassManagerInternal.h:89:3
#17 0x00007f99a5ddfa0e llvm::PassManager<llvm::Function, llvm::AnalysisManager<llvm::Function> >::run(llvm::Function&, llvm::AnalysisManager<llvm::Function>&) (/lib/x86_64-linux-gnu/libLLVM-14.so.1+0xfaea0e)
#18 0x00007f99a79ca24d (/lib/x86_64-linux-gnu/libLLVM-14.so.1+0x2b9924d)
#19 0x00007f99a5de39d1 llvm::ModuleToFunctionPassAdaptor::run(llvm::Module&, llvm::AnalysisManager<llvm::Module>&) (/lib/x86_64-linux-gnu/libLLVM-14.so.1+0xfb29d1)
#20 0x00007f99a79ca07d (/lib/x86_64-linux-gnu/libLLVM-14.so.1+0x2b9907d)
#21 0x00007f99a5dde60e llvm::PassManager<llvm::Module, llvm::AnalysisManager<llvm::Module> >::run(llvm::Module&, llvm::AnalysisManager<llvm::Module>&) (/lib/x86_64-linux-gnu/libLLVM-14.so.1+0xfad60e)
#22 0x00007f99acf65b9b (/lib/x86_64-linux-gnu/libclang-cpp.so.14+0x1862b9b)
#23 0x00007f99acf59a52 clang::EmitBackendOutput(clang::DiagnosticsEngine&, clang::HeaderSearchOptions const&, clang::CodeGenOptions const&, clang::TargetOptions const&, clang::LangOptions const&, llvm::StringRef, llvm::Module*, clang::BackendAction, std::unique_ptr<llvm::raw_pwrite_stream, std::default_delete<llvm::raw_pwrite_stream> >) (/lib/x86_64-linux-gnu/libclang-cpp.so.14+0x1856a52)
#24 0x00007f99ad27f855 (/lib/x86_64-linux-gnu/libclang-cpp.so.14+0x1b7c855)
#25 0x00007f99ac107824 clang::ParseAST(clang::Sema&, bool, bool) (/lib/x86_64-linux-gnu/libclang-cpp.so.14+0xa04824)
#26 0x00007f99ad27bb71 clang::CodeGenAction::ExecuteAction() (/lib/x86_64-linux-gnu/libclang-cpp.so.14+0x1b78b71)
#27 0x00007f99adc17b57 clang::FrontendAction::Execute() (/lib/x86_64-linux-gnu/libclang-cpp.so.14+0x2514b57)
#28 0x00007f99adb6f3a6 clang::CompilerInstance::ExecuteAction(clang::FrontendAction&) (/lib/x86_64-linux-gnu/libclang-cpp.so.14+0x246c3a6)
#29 0x00007f99adc9145b clang::ExecuteCompilerInvocation(clang::CompilerInstance*) (/lib/x86_64-linux-gnu/libclang-cpp.so.14+0x258e45b)
#30 0x000000000041328b cc1_main(llvm::ArrayRef<char const*>, char const*, void*) (/usr/lib/llvm-14/bin/clang+++0x41328b)
#31 0x00000000004114bc (/usr/lib/llvm-14/bin/clang+++0x4114bc)
#32 0x00007f99ad7eded2 (/lib/x86_64-linux-gnu/libclang-cpp.so.14+0x20eaed2)
#33 0x00007f99a5b9cb6d llvm::CrashRecoveryContext::RunSafely(llvm::function_ref<void ()>) (/lib/x86_64-linux-gnu/libLLVM-14.so.1+0xd6bb6d)
#34 0x00007f99ad7ed9c0 clang::driver::CC1Command::Execute(llvm::ArrayRef<llvm::Optional<llvm::StringRef> >, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >*, bool*) const (/lib/x86_64-linux-gnu/libclang-cpp.so.14+0x20ea9c0)
#35 0x00007f99ad7b8183 clang::driver::Compilation::ExecuteCommand(clang::driver::Command const&, clang::driver::Command const*&) const (/lib/x86_64-linux-gnu/libclang-cpp.so.14+0x20b5183)
#36 0x00007f99ad7b840a clang::driver::Compilation::ExecuteJobs(clang::driver::JobList const&, llvm::SmallVectorImpl<std::pair<int, clang::driver::Command const*> >&) const (/lib/x86_64-linux-gnu/libclang-cpp.so.14+0x20b540a)
#37 0x00007f99ad7d2507 clang::driver::Driver::ExecuteCompilation(clang::driver::Compilation&, llvm::SmallVectorImpl<std::pair<int, clang::driver::Command const*> >&) (/lib/x86_64-linux-gnu/libclang-cpp.so.14+0x20cf507)
#38 0x0000000000410f26 main (/usr/lib/llvm-14/bin/clang+++0x410f26)
#39 0x00007f99a48fcd90 __libc_start_call_main ./csu/../sysdeps/nptl/libc_start_call_main.h:58:16
#40 0x00007f99a48fce40 call_init ./csu/../csu/libc-start.c:128:20
#41 0x00007f99a48fce40 __libc_start_main ./csu/../csu/libc-start.c:379:5
#42 0x000000000040e3b5 _start (/usr/lib/llvm-14/bin/clang+++0x40e3b5)
clang: error: clang frontend command failed with exit code 139 (use -v to see invocation)
Ubuntu clang version 14.0.0-1ubuntu1.1
Target: x86_64-pc-linux-gnu
Thread model: posix
InstalledDir: /usr/lib/llvm-14/bin
clang: note: diagnostic msg: 
********************

PLEASE ATTACH THE FOLLOWING FILES TO THE BUG REPORT:
Preprocessed source(s) and associated run script(s) are located at:
clang: note: diagnostic msg: /tmp/UtilityFunctions-5d4db6.cpp
clang: note: diagnostic msg: /tmp/UtilityFunctions-5d4db6.sh
clang: note: diagnostic msg: 

********************
make[3]: *** [CMakeFiles/build.make:244: CMakeFiles/source.cpp.o] Error 139
make[2]: *** [CMakeFiles/Makefile2:295: CMakeFiles/all] Error 2
sebastianpoeplau commented 7 months ago

The crash on your C example is probably caused by SymCC not expecting arithmetic on Booleans. In handwritten code you can do something like !var, but I see that this is difficult with auto-generated code. We should probably add support for arithmetic on Booleans - would you like to give it a try?

The C++ problem looks as if the code was using vector types (e.g., for SIMD instructions), either directly or as a consequence of optimization. These aren't supported in SymCC unfortunately.

exatoa commented 4 months ago

Thanks for the response, @sebastianpoeplau

For C, I think I need to exclude such mutants at this point.

Hope that SymCC supports such an operator and for C++ features soon.