Build process for MathSAT5 for 32bit architectures

[PhilippWendler]

We have decided that we won't build and ship 32bit binaries for solvers, but that we keep JavaSMT compatible to non-x86_64 platforms such that it works if people build and use their own solver binaries.

For this, we need to document for users how to build the respective binaries.

Furthermore, for MathSAT the build process on 32bit machines is broken because the compile.sh no longer accepts a path to the GMP lib but hard-codes the 64bit binaries that we have checked in.

There are also some compiler warnings for the MathSAT bindings on 32bit binaries, which we should check whether they actually break the code:

org_sosy_1lab_solver_mathsat5_Mathsat5NativeApi.c: In function 'Java_org_sosy_1lab_solver_mathsat5_Mathsat5NativeApi_msat_1get_1array_1index_1type':
org_sosy_1lab_solver_mathsat5_Mathsat5NativeApi.c:271:10: warning: cast from pointer to integer of different size [-Wpointer-to-int-cast]
org_sosy_1lab_solver_mathsat5_Mathsat5NativeApi.c: In function 'Java_org_sosy_1lab_solver_mathsat5_Mathsat5NativeApi_msat_1get_1array_1element_1type':
org_sosy_1lab_solver_mathsat5_Mathsat5NativeApi.c:285:10: warning: cast from pointer to integer of different size [-Wpointer-to-int-cast]

[cheshire]

Now this is only specific to MathSAT, as Z3 users can simply use shared objects produced by Z3. Whew!

Maybe we could apply the same approach to MathSAT where we would also use their shared object, which would obliviate the need for the build step altogether?

[cheshire]

@PhilippWendler before I start emailing Mathsat5 team about the possibility of changing the error handling, are we positively sure we need those non-null checks? Have there ever been a case that the returned number was null? Why would it even be null since in C things are usually undefined unless they were assigned to? Why that error condition specifically?

[PhilippWendler]

What do you mean? What error handling? What null checks? This ticket is about documentation and build scripts.

[cheshire]

The best way to solve the ticket is not to have build scripts at all (save
the hack for glibc version). We use our own JNI instead of Mathsat one
because of extra error handling.
On Jun 6, 2016 08:34, "Philipp Wendler" notifications@github.com wrote:

What do you mean? What error handling? What null checks? This ticket is
about documentation and build scripts.

—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
#44 (comment),
or mute the thread
https://github.com/notifications/unsubscribe/AAVTH8ka7nubLstIJpdK4xYXtzXzfyc6ks5qI79qgaJpZM4H9i3A
.

[PhilippWendler]

Yes, this is documented in the MathSAT API: Most term returning functions can return an error term, and we check for this and throw an exception with the appropriate error message instead. This is very useful.

There is also error handling regarding the allocation of memory in our wrapper (using malloc or JNI methods such as NewLongArray) or other calls to JNI methods that is missing in the official API.

All this error handling was added to avoid segfaults. Because segfaults are impossible to handle and will crash your whole application, and because they are so hard to debug, it is IMO important that we do everything that is possible to avoid them in the first place. I actually find this quite lacking when working with Z3, and I would be glad if we had these checks for Z3, too. (Just recently I had to debug and fix bugs leading to segfaults that would have been caught by the very error handling that we have for MathSAT)

[cheshire]

@PhilippWendler But Z3 JNI does check for an error (this is done with a separate function) after every function call.
Are you sure the segfaults you were dealing with are related?

[PhilippWendler]

Yes, I accidentally passed null as an ast argument to Z3, which led to a segfault.

[cheshire]

I think a pull request adding such checks in Native.java file for Z3 is
likely to be accepted. I can do that if you like.

On Thu, Jul 7, 2016 at 4:58 PM, Philipp Wendler notifications@github.com
wrote:

Yes, I accidentally passed null as an ast argument to Z3, which lead to a
segfault.

—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
#44 (comment),
or mute the thread
https://github.com/notifications/unsubscribe/AAVTH3LzpBC9yDJ5AQOlQQKoNgjtb5Z9ks5qTRP6gaJpZM4H9i3A
.

[PhilippWendler]

I you want to take up this effort, sure, why not?

[cheshire]

@PhilippWendler Actually Native.java operates over primitives, which are non-null by definition.
[of course we could check for zeros, but it starts to get ridiculous]
In this case the error checking has to be on our side.
Could you list such methods where you get segfaults?

[PhilippWendler]

A 0 in Java is a null in C, so this is exactly what we check for MathSAT, and which would have prevented the segfault I got (the method was isApp, and the segfault is now already fixed).

Though I think this discussion has nothing to do with the fact that the build process for MathSAT binaries still needs to be fixed and documented.

[cheshire]

@PhilippWendler yes but we have far too many threads for two people already.
0 does correspond to null, but how does zero appear in Java-land?

[PhilippWendler]

I think it is far worse to mix a lot of different stuff in threads. How will somebody find this discussion later on?

In this case, zero appeared as a result of a Z3 method (legally) and was not checked. My point is not about this concrete case, but such things can happen and if we have a code generator like for MathSAT that automatically adds checks everywhere, this is a one-time effort that can detect such bugs easily and always, before we have to invest the effort of debugging a segfault.