eurecom-s3
Could not compile libcxx: malloc/malloc.h not found
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.
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.
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)
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
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.
No problem, I'll close it for now, let us know if you succeed to build the libcxx with SymCC.
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.
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 ?