search

epfl-lara / ScalaZ3

DSL in Scala for Constraint Solving with Z3 SMT Solver
Apache License 2.0
122 stars 34 forks source link

Problem building ScalaZ3 on OSX 10.9 (64b) #28

Closed bcandeias closed 10 years ago

bcandeias commented 10 years ago

Hello all,

I'm trying to build ScalaZ3 but I'm struggling with some errors in the sbt package command. I followed closely all the steps in the README file.

Z3

I'm currently using the unstable version of Z3. I successfully (?) compiled it using

CXX=clang++ CC=clang python scripts/mk_make.py
cd build ; make

Although I saw some warnings coming up, it ended without errors.

I then run sudo make install to finish the installation.

ScalaZ3

I downloaded ScalaZ3-2.9.x and created the path z3/4.3-osx-64b/include and z3/4.3-osx-64b/lib inside it. I then copied z3 include and lib files to them, as ordered.

After that, I ran sbt package and got the following output:

Note: I'm using sbt 0.12.4

bcandeias:ScalaZ3-2.9.x$ sbt package

[info] Loading project definition from /Users/bcandeias/apps/ScalaZ3-2.9.x/project
[info] Set current project to ScalaZ3 (in build file:/Users/bcandeias/apps/ScalaZ3-2.9.x/)
[info] Generating library checksum
[info] Compiling C sources ...
[info] $ gcc -o /Users/bcandeias/apps/ScalaZ3-2.9.x/lib-bin/libscalaz3.dylib -dynamiclib -I/Library/Java/JavaVirtualMachines/jdk1.7.0_40.jdk/Contents/Home/jre/../include -I/System/Library/Frameworks/JavaVM.framework/Versions/Current/Headers -I/Users/bcandeias/apps/ScalaZ3-2.9.x/z3/4.3-osx-64b/include -L/Users/bcandeias/apps/ScalaZ3-2.9.x/z3/4.3-osx-64b/lib -g -lc -lz3 -fPIC -O2 -fopenmp /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/casts.c /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/extra.c /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/z3_thycallbacks.c /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/z3_Z3Wrapper.c
[info] Wrote checksum cc18447f2ae7368241d1ba2ada01aa9 as part of /Users/bcandeias/apps/ScalaZ3-2.9.x/src/main/java/z3/LibraryChecksum.java.
[error] /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/extra.c:24:86: error: non-void function 'parseSMTLIBStringCommon' should return a value [-Wreturn-type]
[error]             jsorts = (*env)->GetLongArrayElements(env, sorts, NULL); if(jsorts == 0) return;
[error]                                                                                      ^
[error] /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/extra.c:25:92: error: non-void function 'parseSMTLIBStringCommon' should return a value [-Wreturn-type]
[error]             jsortsN = (*env)->GetLongArrayElements(env, sortNames, NULL); if(jsortsN == 0) return;
[error]                                                                                            ^
[error] /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/extra.c:28:86: error: non-void function 'parseSMTLIBStringCommon' should return a value [-Wreturn-type]
[error]             jdecls = (*env)->GetLongArrayElements(env, decls, NULL); if(jdecls == 0) return;
[error]                                                                                      ^
[error] /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/extra.c:29:92: error: non-void function 'parseSMTLIBStringCommon' should return a value [-Wreturn-type]
[error]             jdeclsN = (*env)->GetLongArrayElements(env, declNames, NULL); if(jdeclsN == 0) return;
[error]                                                                                            ^
[error] /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/extra.c:40:15: warning: assigning to 'const jbyte *' (aka 'const signed char *') from 'const char *' converts between pointers to integer types with different sign [-Wpointer-sign]
[error]         z3str = (*env)->GetStringUTFChars(env, str, NULL); if (z3str == NULL) return;
[error]               ^ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
[error] /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/extra.c:40:79: error: non-void function 'parseSMTLIBStringCommon' should return a value [-Wreturn-type]
[error]         z3str = (*env)->GetStringUTFChars(env, str, NULL); if (z3str == NULL) return;
[error]                                                                               ^
[error] /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/extra.c:93:86: error: non-void function 'parseSMTLIBFileCommon' should return a value [-Wreturn-type]
[error]             jsorts = (*env)->GetLongArrayElements(env, sorts, NULL); if(jsorts == 0) return;
[error]                                                                                      ^
[error] /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/extra.c:94:92: error: non-void function 'parseSMTLIBFileCommon' should return a value [-Wreturn-type]
[error]             jsortsN = (*env)->GetLongArrayElements(env, sortNames, NULL); if(jsortsN == 0) return;
[error]                                                                                            ^
[error] /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/extra.c:97:86: error: non-void function 'parseSMTLIBFileCommon' should return a value [-Wreturn-type]
[error]             jdecls = (*env)->GetLongArrayElements(env, decls, NULL); if(jdecls == 0) return;
[error]                                                                                      ^
[error] /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/extra.c:98:92: error: non-void function 'parseSMTLIBFileCommon' should return a value [-Wreturn-type]
[error]             jdeclsN = (*env)->GetLongArrayElements(env, declNames, NULL); if(jdeclsN == 0) return;
[error]                                                                                            ^
[error] /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/extra.c:109:15: warning: assigning to 'const jbyte *' (aka 'const signed char *') from 'const char *' converts between pointers to integer types with different sign [-Wpointer-sign]
[error]         z3str = (*env)->GetStringUTFChars(env, str, NULL); if (z3str == NULL) return;
[error]               ^ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
[error] /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/extra.c:109:79: error: non-void function 'parseSMTLIBFileCommon' should return a value [-Wreturn-type]
[error]         z3str = (*env)->GetStringUTFChars(env, str, NULL); if (z3str == NULL) return;
[error]                                                                               ^
[error] 2 warnings and 10 errors generated.
[info] Updating {file:/Users/bcandeias/apps/ScalaZ3-2.9.x/}ScalaZ3...
[error] /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c/z3_Z3Wrapper.c:1:10: fatal error: 'z3_Z3Wrapper.h' file not found
[error] #include "z3_Z3Wrapper.h"
[error]          ^
[error] 1 error generated.
[info] Resolving org.scalatest#scalatest_2.9.3;1.9.1 ...
[info] Done updating.
[info] Compiling 28 Scala sources and 14 Java sources to /Users/bcandeias/apps/ScalaZ3-2.9.x/target/scala-2.9.3/classes...
[info] Preparing JNI headers...
[info] $ javah -classpath /Users/bcandeias/apps/ScalaZ3-2.9.x/target/scala-2.9.3/classes -d /Users/bcandeias/apps/ScalaZ3-2.9.x/src/c z3.Z3Wrapper
[error] Cannot find annotation method 'bytes()' in type 'scala.reflect.ScalaSignature': class file for scala.reflect.ScalaSignature not found
[error] Error: Class scala.ScalaObject could not be found.
[info] Packaging /Users/bcandeias/apps/ScalaZ3-2.9.x/target/scala-2.9.3/scalaz3_2.9.3-2.0.jar ...
[info] Done packaging.
[success] Total time: 56 s, completed 3/Fev/2014 22:43:08

The file target/scala-2.9.3/scalaz3_2.9.3-2.0.jarwas created, tough.

Then running DYLD_LIBRARY_PATH=z3/4.3-osx-64b/lib sbt test I get

bcandeias:ScalaZ3-2.9.x$ DYLD_LIBRARY_PATH=z3/4.3-osx-64b/lib sbt test

[info] Loading project definition from /Users/bcandeias/apps/ScalaZ3-2.9.x/project
[info] Set current project to ScalaZ3 (in build file:/Users/bcandeias/apps/ScalaZ3-2.9.x/)
[info] Generating library checksum
[info] Wrote checksum cc18447f2ae7368241d1ba2ada01aa9 as part of /Users/bcandeias/apps/ScalaZ3-2.9.x/src/main/java/z3/LibraryChecksum.java.
[info] Quantifiers:
Exception in thread "Thread-1" java.io.EOFException
    at java.io.ObjectInputStream$BlockDataInputStream.peekByte(ObjectInputStream.java:2597)
    at java.io.ObjectInputStream.readObject0(ObjectInputStream.java:1316)
    at java.io.ObjectInputStream.readObject(ObjectInputStream.java:370)
    at sbt.React.react(ForkTests.scala:98)
    at sbt.ForkTests$$anonfun$apply$2$Acceptor$2$.run(ForkTests.scala:66)
    at java.lang.Thread.run(Thread.java:724)
[info] Passed: : Total 0, Failed 0, Errors 0, Passed 0, Skipped 0
[info] No tests to run for test:test
[success] Total time: 3 s, completed 3/Fev/2014 22:48:20

Does anyone know what's going on? Am I doing something wrong?

Thanks in advance!

koksal commented 10 years ago

My guess is that this is due to OS X aliasing gcc to clang. Running sbt package with the actual gcc might resolve the compilation errors.

colder commented 10 years ago

We recently fixed some compilation errors and/or adjusted the sensitivity of the compiler. We also fixed issues with the packaging process for mac-osx. Please re-open if the latest version does not fix your issue.