search

epfl-lara / ScalaZ3

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

Can the hand-written JNI code be replaced with JNR-FFI? #45

Closed JoshRosen closed 7 years ago

JoshRosen commented 9 years ago

Is there a reason why ScalaZ3 needs to use hand-written JNI code instead of JNR-FFI? Removing the need to package custom native code would allow cross-platform ScalaZ3 JARs to be published on Maven; users would only have to ensure that an appropriate version of the libz3 was on their runtime includes path.

JoshRosen commented 9 years ago

I spent a bit of time porting ScalaZ3 to use JNR-FFI; you can find my work-in-progress code at https://github.com/JoshRosen/ScalaZ3/compare/jnr?diff=unified&expand=1&name=jnr (I'll open a pull request once it's a bit more complete).

A handful of things are broken, including TheoryProxy, and the Quantifiers suite is currently failing with a core dump (so I've probably made a low-level mistake somewhere), but the other test suites seem to pass. The switch to JNR let me remove all of the native code from the build, which will significantly simplify packaging and distribution.

The bulk of these changes were done semi-automatically using some hacky Python and sed; I had to do a bit of manual tinkering to fix up some cases where the order of parameters passed to the JNI wrapper did not match the order expected by the underlying Z3 call. I haven't looked into performance impacts yet, but note that I haven't spent too much time looking at annotations like @In and @Out to avoid copying, so it's possible that there's still a ways to go in terms of reducing the native call overhead.

samarion commented 7 years ago

You're quite right, maintaining the manually written JNI was infeasible. Luckily for us, Z3 now ships with a Java interface which contains some automatically generated JNI, so that's what we're relying on currently.