depqbf icon indicating copy to clipboard operation
depqbf copied to clipboard

symbol(s) not found for architecture arm64

Open Alexanderia-Mike opened this issue 4 years ago • 2 comments

I'm using MacBook M1 with arm64 architecture. I'm trying to compile the package into a static library, and I type ./compile.sh in the terminal, but the process seems unsuccessful. There are following lines indicating some symbols are not found for architecture arm64:

Undefined symbols for architecture arm64:
  "_picosat_add", referenced from:
      _nnf_to_cnf_forward in nenofex.fpico
      _nnf_to_cnf_standard_tseitin_forward in nenofex.fpico
  "_picosat_decisions", referenced from:
      _nenofex_solve in nenofex.fpico
  "_picosat_deref", referenced from:
      _nenofex_solve in nenofex.fpico
  "_picosat_init", referenced from:
      _nenofex_solve in nenofex.fpico
  "_picosat_reset", referenced from:
      _nenofex_solve in nenofex.fpico
  "_picosat_sat", referenced from:
      _nenofex_solve in nenofex.fpico
  "_picosat_set_verbosity", referenced from:
      _nenofex_solve in nenofex.fpico
ld: symbol(s) not found for architecture arm64
clang: error: linker command failed with exit code 1 (use -v to see invocation)
make: *** [libnenofex.1.1.dylib] Error 1

I'm a beginner in programming and did not know much about shellscripts or things like that. I'm wondering why the above errors occur and how I can possibly fix them. Any ideas or advices are greatly appropriated! Thanks!

The whole outputs in the terminal are what follows:

Found directory 'picosat'
version ... 960
debug ... no
log ... no
stats ... no
trace ... no
static ... no
shared ... no
targets ... picosat picomcs picomus picogcnf libpicosat.a
cc ... gcc
cflags ...  -Wall -Wextra -DNDEBUG -O3
makefile ... done
gcc -Wall -Wextra -DNDEBUG -O3 -c picosat.c
rm -f config.h; ./mkconfig > config.h
gcc -Wall -Wextra -DNDEBUG -O3 -c version.c
ar rc libpicosat.a picosat.o version.o
ranlib libpicosat.a
gcc -Wall -Wextra -DNDEBUG -O3 -c app.c
gcc -Wall -Wextra -DNDEBUG -O3 -c main.c
gcc -Wall -Wextra -DNDEBUG -O3 -o picosat main.o app.o -L. -lpicosat
gcc -Wall -Wextra -DNDEBUG -O3 -c picomcs.c
gcc -Wall -Wextra -DNDEBUG -O3 -o picomcs picomcs.o -L. -lpicosat
gcc -Wall -Wextra -DNDEBUG -O3 -c picomus.c
gcc -Wall -Wextra -DNDEBUG -O3 -o picomus picomus.o -L. -lpicosat
gcc -Wall -Wextra -DNDEBUG -O3 -c picogcnf.c
gcc -Wall -Wextra -DNDEBUG -O3 -o picogcnf picogcnf.o -L. -lpicosat
Found directory 'nenofex'
ar rc libnenofex.a nenofex.o stack.o queue.o mem.o atpg.o ../picosat/picosat.o
ranlib libnenofex.a
cc  -shared -Wl,-install_name,libnenofex.1.dylib nenofex.fpico stack.fpico queue.fpico mem.fpico atpg.fpico -o libnenofex.1.1.dylib
Undefined symbols for architecture arm64:
  "_picosat_add", referenced from:
      _nnf_to_cnf_forward in nenofex.fpico
      _nnf_to_cnf_standard_tseitin_forward in nenofex.fpico
  "_picosat_decisions", referenced from:
      _nenofex_solve in nenofex.fpico
  "_picosat_deref", referenced from:
      _nenofex_solve in nenofex.fpico
  "_picosat_init", referenced from:
      _nenofex_solve in nenofex.fpico
  "_picosat_reset", referenced from:
      _nenofex_solve in nenofex.fpico
  "_picosat_sat", referenced from:
      _nenofex_solve in nenofex.fpico
  "_picosat_set_verbosity", referenced from:
      _nenofex_solve in nenofex.fpico
ld: symbol(s) not found for architecture arm64
clang: error: linker command failed with exit code 1 (use -v to see invocation)
make: *** [libnenofex.1.1.dylib] Error 1
cc -Wextra -Wall -Wno-unused-parameter -Wno-unused -pedantic -std=c99 -DNDEBUG -O3  -c qdpll_main.c -o qdpll_main.o
cc -Wextra -Wall -Wno-unused-parameter -Wno-unused -pedantic -std=c99 -DNDEBUG -O3  -c qdpll_app.c -o qdpll_app.o
cc -Wextra -Wall -Wno-unused-parameter -Wno-unused -pedantic -std=c99 -DNDEBUG -O3  -c qdpll.c -o qdpll.o
qdpll.c:6809:24: warning: format specifies type 'int' but the argument has type 'long' [-Wformat]
                       sp - qdpll->qbcp_qbce_blocked_clauses.start);
                       ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
qdpll.c:11414:77: warning: format specifies type 'unsigned int' but the argument has type 'size_t' (aka 'unsigned long') [-Wformat]
      fprintf (stderr, "WATCHING: deleting list entry, new list size %u\n", QDPLL_COUNT_STACK (*list));
                                                                     ~~     ^~~~~~~~~~~~~~~~~~~~~~~~~
                                                                     %zu
./qdpll_stack.h:55:34: note: expanded from macro 'QDPLL_COUNT_STACK'
#define QDPLL_COUNT_STACK(stack) ((size_t) ((stack).top - (stack).start))
                                 ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
qdpll.c:12609:42: warning: format specifies type 'unsigned int' but the argument has type 'size_t' (aka 'unsigned long') [-Wformat]
                                         QDPLL_COUNT_STACK (*occs), qdpll->options.qbcp_qbce_find_witness_max_occs);
                                         ^~~~~~~~~~~~~~~~~~~~~~~~~
./qdpll_stack.h:55:34: note: expanded from macro 'QDPLL_COUNT_STACK'
#define QDPLL_COUNT_STACK(stack) ((size_t) ((stack).top - (stack).start))
                                 ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3 warnings generated.
cc -Wextra -Wall -Wno-unused-parameter -Wno-unused -pedantic -std=c99 -DNDEBUG -O3  -c qdpll_dep_man_qdag.c -o qdpll_dep_man_qdag.o
ar rc libqdpll.a qdpll.o qdpll_pqueue.o qdpll_mem.o qdpll_dep_man_qdag.o qdpll_dynamic_nenofex.o nenofex/nenofex.o nenofex/stack.o nenofex/queue.o nenofex/mem.o nenofex/atpg.o picosat/picosat.o
ranlib libqdpll.a
cc -Wextra -Wall -Wno-unused-parameter -Wno-unused -pedantic -std=c99 -DNDEBUG -O3  -fPIC -c qdpll.c -o qdpll.fpico
qdpll.c:6809:24: warning: format specifies type 'int' but the argument has type 'long' [-Wformat]
                       sp - qdpll->qbcp_qbce_blocked_clauses.start);
                       ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
qdpll.c:11414:77: warning: format specifies type 'unsigned int' but the argument has type 'size_t' (aka 'unsigned long') [-Wformat]
      fprintf (stderr, "WATCHING: deleting list entry, new list size %u\n", QDPLL_COUNT_STACK (*list));
                                                                     ~~     ^~~~~~~~~~~~~~~~~~~~~~~~~
                                                                     %zu
./qdpll_stack.h:55:34: note: expanded from macro 'QDPLL_COUNT_STACK'
#define QDPLL_COUNT_STACK(stack) ((size_t) ((stack).top - (stack).start))
                                 ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
qdpll.c:12609:42: warning: format specifies type 'unsigned int' but the argument has type 'size_t' (aka 'unsigned long') [-Wformat]
                                         QDPLL_COUNT_STACK (*occs), qdpll->options.qbcp_qbce_find_witness_max_occs);
                                         ^~~~~~~~~~~~~~~~~~~~~~~~~
./qdpll_stack.h:55:34: note: expanded from macro 'QDPLL_COUNT_STACK'
#define QDPLL_COUNT_STACK(stack) ((size_t) ((stack).top - (stack).start))
                                 ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3 warnings generated.
cc -Wextra -Wall -Wno-unused-parameter -Wno-unused -pedantic -std=c99 -DNDEBUG -O3  -fPIC -c qdpll_dep_man_qdag.c -o qdpll_dep_man_qdag.fpico
cc -L./picosat/ -lpicosat -L./nenofex -lnenofex -shared -Wl,-install_name,libqdpll.1.dylib qdpll.fpico qdpll_pqueue.fpico qdpll_mem.fpico qdpll_dep_man_qdag.fpico qdpll_dynamic_nenofex.fpico -o libqdpll.1.0.dylib
cc -Wextra -Wall -Wno-unused-parameter -Wno-unused -pedantic -std=c99 -DNDEBUG -O3  qdpll_main.o qdpll_app.o -L. -lqdpll -o depqbf

Alexanderia-Mike avatar Mar 29 '21 11:03 Alexanderia-Mike

Thanks for pointing this out! The problem seems to be related to producing dynamic libraries on macOS/arm64.

If you only want to produce a static library, you can disable the production of dynamic libraries by running the following steps in a clean directory of depqbf (these are from the compile.sh script with some modifications).

wget http://fmv.jku.at/picosat/picosat-960.tar.gz
tar -xvzf picosat-960.tar.gz
mv picosat-960 picosat

cd picosat
./configure
make
cd ..

wget https://github.com/lonsing/nenofex/archive/version-1.1.tar.gz
tar -xvzf version-1.1.tar.gz
mv nenofex-version-1.1 nenofex

cd nenofex

Now change the makefile of Nenofex (./nenofex/makefile) by removing the following lines:

ifeq ($(UNAME), Darwin)
# Mac OS X
SONAME=-install_name
TARGETS+=libnenofex.$(VERSION).dylib
else
SONAME=-soname
TARGETS+=libnenofex.so.$(VERSION)
endif

Then run:

make
cd ..

Now change the makefile of DepQBF (./depqbf/makefile) by removing the following lines:

ifeq ($(UNAME), Darwin)
# Mac OS X
SONAME=-install_name
TARGETS+=libqdpll.$(VERSION).dylib
else
SONAME=-soname
TARGETS+=libqdpll.so.$(VERSION)
endif

And change line

$(CC) $(CFLAGS) qdpll_main.o qdpll_app.o -L. -lqdpll -o depqbf

to

$(CC) $(CFLAGS) -static qdpll_main.o qdpll_app.o -L. -lqdpll -o depqbf

and then run

make

That should produce a static binary ./depqbf.

lonsing avatar Mar 31 '21 16:03 lonsing

Thank you so much for your detailed reply!

The problem about "arm64" has gone. There is only one issue left, that is the flag "-static" seems to be incompatible with CC in Mac OS Clang, as every time I tried to run depqbf/makefile, the command line complains that

ld: library not found for -lcrt0.o

And after some research online, it seems to be a problem of "-static" flag in Mac OS. The answer in this StackOverflow page says that: This option will not work on Mac OS X unless all libraries (including libgcc.a) have also been compiled with -static. Since neither a static version of libSystem.dylib nor crt0.o are provided, this option is not useful to most people.

I suppose that it's only a problem about finding a proper substitution for "-static" in Mac OS, and I'm trying to figure out how to do that by myself. Hopefully I can manage that.

Anyway, much thanks!

Alexanderia-Mike avatar Apr 04 '21 04:04 Alexanderia-Mike