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
771 stars 137 forks source link

Could not compile libcxx: malloc/malloc.h not found #147

Open aur3l14no opened 11 months ago

aur3l14no commented 11 months ago

SymCC is compiled successfully. But building libcxx got me these errors (during configuration).

export SYMCC_REGULAR_LIBCXX=yes
export SYMCC_NO_SYMBOLIC_INPUT=yes

cmake -G Ninja /workspace/llvm-project/llvm \
      -DLLVM_ENABLE_RUNTIMES="libcxx;libcxxabi" \
      -DLLVM_TARGETS_TO_BUILD="X86" \
      -DLLVM_DISTRIBUTION_COMPONENTS="cxx;cxxabi;cxx-headers" \
      -DCMAKE_BUILD_TYPE=Release \
      -DCMAKE_INSTALL_PREFIX=/home/vscode/libcxx_symcc \
      -DCMAKE_C_COMPILER=/workspace/symcc/build/symcc \
      -DCMAKE_CXX_COMPILER=/workspace/symcc/build/sym++
/workspace/symcc/build/symcc   -O3 -DNDEBUG -o CMakeFiles/cmTC_a2a0a.dir/CheckIncludeFile.c.o   -c CheckIncludeFile.c
CheckIncludeFile.c:1:10: fatal error: 'malloc/malloc.h' file not found
#include <malloc/malloc.h>
         ^~~~~~~~~~~~~~~~~
1 error generated.
ninja: build stopped: subcommand failed.

...
fatal error: 'mach/mach.h' file not found
fatal error: 'CrashReporterClient.h' file not found
...

Kindly, any advice on how to fix this error would be appreciated.

aurelf commented 11 months ago

I'm not sure how much the LibCXX instructions are still up to date. If you followed the instructions in docs/C++.txt you used the current git version of the LLVM project? There may be breaking changes. Can you try compiling against LLVM-16 or 15 ? We should support those versions.

aurelf commented 11 months ago

An alternative is to rely on the docker files libcxx seem to work there (although I see there are issues with the symcc_fuzzing_helper but this is another problem)

aur3l14no commented 11 months ago

I actually was using LLVM-16 (16.0.6), which is built and installed via

cmake -DCMAKE_BUILD_TYPE=Release \
      -DLLVM_ENABLE_PROJECTS="clang" \
      -DLLVM_ENABLE_RUNTIMES="libcxx;libcxxabi;libunwind" \
      -DLLVM_TARGETS_TO_BUILD="X86" \
      -G Ninja /workspace/llvm-project/llvm
cmake --build .
cmake --build . --target install
aur3l14no commented 11 months ago

Oh... I realized that I even failed to build cxx with clang. I think it's not an issue with symcc then. Sorry for bothering.

aurelf commented 11 months ago

No problem, I'll close it for now, let us know if you succeed to build the libcxx with SymCC.

aur3l14no commented 11 months ago

Hey @aurelf I'd like to update that I have built libcxx successfully, but with somewhat different configs.

cmake -G Ninja -S /workspace/llvm-project/runtimes \
      -DCMAKE_BUILD_TYPE=Release \
      -DLLVM_TARGETS_TO_BUILD="X86" \
      -DLLVM_ENABLE_RUNTIMES="libcxx;libcxxabi;libunwind" \
      -DCMAKE_INSTALL_PREFIX=/home/vscode/libcxx_symcc \
      -DCMAKE_C_COMPILER=symcc \
      -DCMAKE_CXX_COMPILER=sym++
ninja cxx cxxabi unwind
ninja install-cxx install-cxxabi install-unwind

Please note that the source directory is changed to runtimes. It seems that with llvm as source dir, I can only perform a 2-stage build (build clang first then runtimes), and I can't just stick a compiled clang (symcc) to replace the first stage otherwise there will be errors (maybe related to cmake files but I didn't investigate further).

Anyways, I followed the guide here (https://releases.llvm.org/16.0.0/projects/libcxx/docs/BuildingLibcxx.html#the-default-build) and came up with the above build command. And it worked.


Also, I had to tweak this line in sym++, otherwise I would see similar errors as in #104

stdlib_cflags="-isystem ${!libcxx_var}/include/c++/v1 -nostdinc++ -nostdlib++"

Going through all that, I finally managed to symbolize the sample.cpp. However, it failed to generate the alternative input although the constraints did somewhat show the answer...

(assert ...)
(assert ...)
(assert (and (= stdin0 #x72) (= stdin1 #x6f) (= stdin2 #x6f) (= stdin3 #x74)))

# the result is unsat

I noticed in the README that, with QSYM, the output is named "xxx_optimistic". Does it mean the result rely on optimistic (underconstrained) solving to become SAT? I haven't been able to build the QSYM backend so I couldn't test it out.

aurelf commented 11 months ago

Thanks for the investigation ! Reopening. Looks like the port to LLVM 16 was not complete, the CI tests need to be improved in that respect :) Unfortunately, I don't have time to look this more before a while. @sebastianpoeplau if you do, could you have a look ?