Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

yices build issues #9

Closed
ianamason opened this issue Jul 20, 2017 · 10 comments
Closed

yices build issues #9

ianamason opened this issue Jul 20, 2017 · 10 comments
Assignees

Comments

@ianamason
Copy link
Member

Seems like there are some bugs with gclang. These give different results:

./configure

vs

CC=gclang ./configure

yields

checking for libgmp.a in /lib64... no
checking for libgmp.a in /usr/lib/x86_64-linux-gnu... found
checking whether /usr/lib/x86_64-linux-gnu/libgmp.a is usable... yes
checking for __gmpz_cmp in -lgmp... yes

vs

checking for libgmp.a in /usr/lib/x86_64-linux-gnu... found
checking whether /usr/lib/x86_64-linux-gnu/libgmp.a is usable... no
checking for libgmp.a in /usr/lib64... no
checking for libgmp.a in /usr/local/lib... no
checking for libgmp.a in /lib... no
checking for libgmp.a in /usr/lib... no
checking for libgmp.a in /usr/local/lib... no
checking for libgmp.a in /usr/lib... no
checking for libgmp.a in /lib... no
configure: WARNING: *** No usable libgmp.a library was found ***
checking for __gmpz_cmp in -lgmp... yes
  1. And the subsequent make with the gclang compiler fails with complaints like:
Makefile:802: ../build/x86_64-unknown-linux-gnu-release/obj/api/context_config.d: No such file or directory
@ianamason ianamason self-assigned this Jul 20, 2017
@ianamason
Copy link
Member Author

Ok so the dependency generation now works. But we still have the following mystery:

iam@shaman:~/Repositories/yices2$ CC=gclang ./configure
...
checking whether /usr/lib/x86_64-linux-gnu/libgmp.a is usable... no

vs

iam@shaman:~/Repositories/yices2$ WLLVM_CONFIGURE_ONLY=1 CC=gclang ./configure
checking whether /usr/lib/x86_64-linux-gnu/libgmp.a is usable... yes

and in the llvm logs we see both returning 0.

Entering [gclang -o conftest -g -O2 conftest.c /usr/lib/x86_64-linux-gnu/libgmp.a -lm]
/usr/local/llvm-3.5/bin/clang [/usr/lib/x86_64-linux-gnu/libgmp.a -lm .conftest.o -o conftest] failed to link: exit status 1.
Calling [gclang -o conftest -g -O2 conftest.c /usr/lib/x86_64-linux-gnu/libgmp.a -lm] returned 0
Entering [gclang -o conftest -g -O2 conftest.c /usr/lib/x86_64-linux-gnu/libgmp.a -lm]
Calling [gclang -o conftest -g -O2 conftest.c /usr/lib/x86_64-linux-gnu/libgmp.a -lm] returned 0

@ianamason
Copy link
Member Author

ianamason commented Jul 21, 2017

gclang -o conftest -g -O2 conftest.c /usr/lib/x86_64-linux-gnu/libgmp.a -lm

where conftest.c is

#include <gmp.h>

mpz_t tst;

int
main ()
{

mpz_init(tst);
mpz_clear(tst);
if ((__GNU_MP_VERSION < 4) ||
    ((__GNU_MP_VERSION == 4) && (__GNU_MP_VERSION_MINOR < 1))) {
    return 1;
  }

  ;
  return 0;
}

we have

iam@shaman:~/Repositories/yices2$ gclang -o conftest -g -O2 conftest.c /usr/lib/x86_64-linux-gnu/libgmp.a -lm
.conftest.o: In function `main':
/home/iam/Repositories/yices2/conftest.c:10: undefined reference to `__gmpz_init'
/home/iam/Repositories/yices2/conftest.c:11: undefined reference to `__gmpz_clear'
clang: error: linker command failed with exit code 1 (use -v to see invocation)
iam@shaman:~/Repositories/yices2echo $?
0
iam@shaman:~/Repositories/yices2$ WLLVM_CONFIGURE_ONLY=1 gclang -o conftest -g -O2 conftest.c /usr/lib/x86_64-linux-gnu/libgmp.a -lm
iam@shaman:~/Repositories/yices2$ echo $?
0

So @BrunoDutertre they seem to have the same exit code, is the stderr triggering failure?
what behaviour is triggering the configure difference?

@ianamason
Copy link
Member Author

WLLVM_CONFIGURE_ONLY=1 gclang -o conftest -g -O2 conftest.c /usr/lib/x86_64-linux-gnu/libgmp.a -lm

Entering [gclang -o conftest -g -O2 conftest.c /usr/lib/x86_64-linux-gnu/libgmp.a -lm]
execCmd: /usr/local/llvm-3.5/bin/clang [-o conftest -g -O2 conftest.c /usr/lib/x86_64-linux-gnu/libgmp.a -lm] in  had exitCode 0
Calling [gclang -o conftest -g -O2 conftest.c /usr/lib/x86_64-linux-gnu/libgmp.a -lm] returned 0
gclang -o conftest -g -O2 conftest.c /usr/lib/x86_64-linux-gnu/libgmp.a -lm
Entering [gclang -o conftest -g -O2 conftest.c /usr/lib/x86_64-linux-gnu/libgmp.a -lm]
execCmd: /usr/local/llvm-3.5/bin/clang [-g -O2 conftest.c -c -o .conftest.o] in  had exitCode 0
execCmd: /usr/local/llvm-3.5/bin/clang [-o conftest -g -O2 conftest.c /usr/lib/x86_64-linux-gnu/libgmp.a -lm] in  had exitCode 0
execCmd: /usr/local/llvm-3.5/bin/clang [-g -O2 -emit-llvm -c conftest.c -o .conftest.o.bc] in  had exitCode 0
execCmd: objcopy [--add-section .llvm_bc=/tmp/gllvm134744506 .conftest.o] in  had exitCode 0
execCmd: /usr/local/llvm-3.5/bin/clang [/usr/lib/x86_64-linux-gnu/libgmp.a -lm .conftest.o -o conftest] in  had exitCode 1
execCmd: error was exit status 1
/usr/local/llvm-3.5/bin/clang [/usr/lib/x86_64-linux-gnu/libgmp.a -lm .conftest.o -o conftest] failed to link: exit status 1.
Calling [gclang -o conftest -g -O2 conftest.c /usr/lib/x86_64-linux-gnu/libgmp.a -lm] returned 0
wllvm -o conftest -g -O2 conftest.c /usr/lib/x86_64-linux-gnu/libgmp.a -lm
DEBUG::compilers.getBuilder() at compilers.py:218 ::WLLVM compiler using clang
DEBUG::compilers.getBuilder() at compilers.py:220 ::WLLVM compiler path prefix "/usr/local/llvm-3.5/bin"
DEBUG::compilers.buildObject() at compilers.py:240 ::buildObject rc = 0
DEBUG::compilers.buildAndAttachBitcode() at compilers.py:279 ::Not compile only case: conftest.c
DEBUG::compilers.buildObjectFile() at compilers.py:333 ::buildObjectFile: ['/usr/local/llvm-3.5/bin/clang', '-g', '-O2', 'conftest.c', '-c', '-o', '.conftest.o']
DEBUG::compilers.buildAndAttachBitcode() at compilers.py:289 ::building and attaching .conftest.o.bc to .conftest.o
DEBUG::compilers.buildBitcodeFile() at compilers.py:320 ::buildBitcodeFile: ['/usr/local/llvm-3.5/bin/clang', '-emit-llvm', '-g', '-O2', '-c', 'conftest.c', '-o', '.conftest.o.bc']
DEBUG::compilers.attachBitcodePathToObject() at compilers.py:95 ::attachBitcodePathToObject: .conftest.o.bc  ===> .conftest.o [ext = .o]
DEBUG::compilers.attachBitcodePathToObject() at compilers.py:107 ::Wrote "/space/Repositories/yices2/.conftest.o.bc" to file "/tmp/tmpXYKvn0"

@ianamason
Copy link
Member Author

Need to instrument the link step in wllvm, but the gclang one looks wrong, since it is missing the native library.

@BrunoDutertre
Copy link
Member

@ianamason: the order matters

Instead of

/usr/local/llvm-3.5/bin/clang [/usr/lib/x86_64-linux-gnu/libgmp.a -lm .conftest.o -o conftest]

the link command should be

/usr/local/llvm-3.5/bin/clang [.conftest.o /usr/lib/x86_64-linux-gnu/libgmp.a -lm -o conftest]

Function compileTimeLinkFiles in compiler.go does not put the arguments in the right
order.

@ianamason
Copy link
Member Author

Ah so. Yes still not sure why the config test is sensitive to what happens in the unnecessary second phase.

@BrunoDutertre
Copy link
Member

Because the code in compiler.go ignores the exec code of the second pass:

wg.Add(2)
go execCompile(compilerExecName, pr, &wg, &ok)
go buildAndAttachBitcode(compilerExecName, pr, &bcObjLinks, &newObjectFiles, &skip, &wg)
wg.Wait()

Then check ok.

@ianamason
Copy link
Member Author

Right. I know that. Not sthupid. So why does the config test fail when the second phase happens,
but succeed when it doesn't?

@BrunoDutertre
Copy link
Member

Because the configure test tries to link and run the test program.

@ianamason
Copy link
Member Author

ianamason commented Jul 22, 2017 via email

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants