search

moyix / fpsmt_gpu

Solving floating point SMT constraints on a GPU
48 stars 2 forks source link

Code doesn't compile #2

Closed pgarba closed 3 years ago

pgarba commented 3 years ago

Hi,

I'm getting this error during compilation:

❯ ./generate.sh sample_smt/readme.smt2
smt2cxx:1: command not found: docker
nvcc --expt-relaxed-constexpr -DJFS_RUNTIME_FAILURE_CALLS_ABORT -dc -std=c++11 -I. -c theory.cu -o theory.o
nvcc --expt-relaxed-constexpr -DJFS_RUNTIME_FAILURE_CALLS_ABORT -dc -std=c++11 -I. -c smt.cu -o smt.o
nvcc --expt-relaxed-constexpr -DJFS_RUNTIME_FAILURE_CALLS_ABORT -dc -std=c++11 -I. -c aes.cu -o aes.o
make -C SMTLIB
make[1]: Entering directory '/home/adam/tools/fpsmt_gpu/SMTLIB'
nvcc --expt-relaxed-constexpr -DJFS_RUNTIME_FAILURE_CALLS_ABORT -dc -std=c++11 -I.. -c Core.cu -o Core.o
nvcc --expt-relaxed-constexpr -DJFS_RUNTIME_FAILURE_CALLS_ABORT -dc -std=c++11 -I.. -c Float.cu -o Float.o
nvcc --expt-relaxed-constexpr -DJFS_RUNTIME_FAILURE_CALLS_ABORT -dc -std=c++11 -I.. -c Logger.cu -o Logger.o
nvcc --expt-relaxed-constexpr -DJFS_RUNTIME_FAILURE_CALLS_ABORT -dc -std=c++11 -I.. -c Messages.cu -o Messages.o
nvcc --expt-relaxed-constexpr -DJFS_RUNTIME_FAILURE_CALLS_ABORT -dc -std=c++11 -I.. -c NativeBitVector.cu -o NativeBitVector.o
nvcc --expt-relaxed-constexpr -DJFS_RUNTIME_FAILURE_CALLS_ABORT -dc -std=c++11 -I.. -c NativeFloat.cu -o NativeFloat.o
make[1]: Leaving directory '/home/adam/tools/fpsmt_gpu/SMTLIB'
nvcc theory.o smt.o aes.o SMTLIB/Core.o SMTLIB/Logger.o SMTLIB/NativeFloat.o SMTLIB/Messages.o SMTLIB/Float.o SMTLIB/NativeBitVector.o -o smt
nvlink error   : Undefined reference to '_Z22LLVMFuzzerTestOneInputPKhm' in 'smt.o'
make: *** [Makefile:18: smt] Error 255

Any idea whats wrong ?

moyix commented 3 years ago

Yes, the code depends on docker in order to run JFS. You need to have docker installed and working in order to run it.