Interaction with Z3 through Z3's Java API instead of StdIO

[marcoeilers]

Requires libz3java to be on the LD_LIBRARY_PATH (or the Windows equivalent) or the java.library.path. The included Java files are from Z3 version 4.8.6, so the library should have the same version, but apparently 4.8.7 also works. Newer versions do not.

Some interesting points:

• Silicon emits lots of function declarations and axioms for various stuff as SMT2LIB strin gbefore verifying stuff. We parse this, but to be able to do this, we need to parse this stuff all at once. So we collect all of this stuff and then parse it all at once (once the preamble is over).
• We pass in settings directly via the API and just ignore settings passed as set-option strings; as a side note, half of the options we use no longer exist in the current Z3 version, and passing non-existing options via API results in an exception.
• We cache function declarations and sort translations.
• Counterexample (model) extraction via API is implemented, too.
• The entire test suite should work, except that there is an example that contains invalid triggers; while this results in a warning when using Z3 via StdIO, it results in an exception when used via API, so that example won't verify.
• To handle built-in SMTLIB functions not directly available in Viper (e.g., bitvectors and floats), we use a bit of a hack, since we cannot use them via API from only a string (they have their own API functions). So we create mini-SMTLIB queries that use those functions, let Z3 parse them, and take what we need from the generated ASTs.

Probably shouldn't be merged before the release.
I measured a 10-40% speedup for examples from the test suite and much higher speedups for some very long running examples.

[Aurel300]

(Note on macOS the equivalent is DYLD_LIBRARY_PATH.)

[Aurel300]

Is this because we don't know the types for the arguments? Are we passing them to Z3 so it can figure out their sorts?

[marcoeilers]

No, the problem is that there is nothing like ctx.getInterpretedFuncDecl(name) in the API that I could give a string like "fp.add" to and get the declaration for floating point addition. Instead, for any built-in interpreted function, there is a separate creator method in the API (e.g., ctx.mkFloatAdd(arg1, arg2)). So I'd have to have a big match-case here that matches all names of all built-in functions and then calls the respectice API method. Which I didn't want to do now because there are a lot of them, and the way we currently use SMTFuncApps, sometimes, the strings aren't actually just a function name but a function name and some number of default argument (e.g., "fp.add RNE", which contains the function name and a first argument that determines the rounding mode).

[Aurel300]

Can this happen for other reasons (e.g. accidentally calling a function with the wrong number of arguments)? Could you whitelist only float-related operations in this branch?

[marcoeilers]

I guess it could, yes.

I think if we want to avoid this special case (which really shouldn't be here), we should just forbid including arguments in the function name in general, then we wouldn't have to handle this case here. It's just that that was unproblematic when we were dealing only with strings, so I did it when making the factory for floating point operations. If we rewrite that code, I think the only consequence is that users of floating point functions would always have to pass the rounding mode explicitly.

[fpoli]

I don't remember if there is anything useful, but you can also check #519.

[Aurel300]

One particular difference I noticed is using a "managed" library for the Z3 APIs in build.sbt, along with some updates to the silicon.sh script to accommodate for this. @marcoeilers is this the same library you are using here? Having a managed dependency is probably better than shipping a JAR like this.

[marcoeilers]

Oh, I only saw your comments just now. Yes, I agree a proper library dependency is much nicer.

[marcoeilers]

As far as I'm concerned, since the release is done now, we could merge this. @mschwerhoff what do you think?

[marcoeilers]

Merged as part of the parallel branch verification PR.