Invariant Solver

[sankalpgambhir]

Adding a solver backend to encode problems as constrained Horn clauses and attempt to produce invariants.

Currently supports recursive first-order integer programs. Experimental support for higher-order functions is implemented using arrays to represent first-class functions.

There are currently two versions: SimpleHornSolver and InvariantSolver. The SimpleHornSolver was created as a modification of the UnrollingSolver but will be removed in favour of the from-scratch InvariantSolver before merge.

Working on getting it to print discovered invariants as additional info. Currently, z3 outputs some models for Horn clauses with syntax outside that accepted by scala-smtlib, which need to be dealt with.

Concrete changelist:

• InvariantSolver: main addition

  • an abstract solver for encoding Inox problems into Horn clauses
  • transforms assertions into constrained Horn clauses
  • transitively adds function definitions from the program encoded as relationized functions
  • the encoding is "SAT as safety"
  • the constraints are discharged by an underlying (SMTLIB) CHC solver
  • the result is flipped as expected of an SMT solver (Inox's expected result)
  • should behave as just another Inox solver, albeit with less support for different datatypes

• SMTLIBSolver / SMTLIBTarget: common SMTLIB solver backend

  • add support for a set of predicate symbols, which are not treated as first-class functions based simply on their types (FunctionType(Seq(...), Boolean))
  • modified the model extraction to not discard models for registered predicate symbols
  • does not affect other solvers; opt-in by using the registerPredicate function
  • removed the unused parseSuccess method that accessed interpreter internals. (checked because the eldarica interpreter is not well-behaved wrt these internal semantics as it does not use IPC like every other interpreter)

• EldaricaInterpreter

  • general purpose backend for eldarica
  • communicates with Eldarica over string streams by just spawning its main function under an executor
  • this mirrors how eldarica is used within its own server mode
  • not battle-tested yet, it should appropriately catch and scream when things unsupported by Eldarica are sent in

• SolverFactory: updated options and factory to make inv-z3 and inv-eld available as solvers

• uuverifiers dependencies

  • updated the maven server to the correct new link at https://eldarica.org/maven (with HTTPS now!)
  • updated princess to resolve as a library instead of a git dependency (eldarica uses princess from maven, so there is a conflict too otherwise)
  • added eldarica as a library dependency
  • these changes produce a weird issue where external dependencies of eldarica are detected as having "conflicting cross-version suffixes" despite not being required by anything else (sbt dependencyTree). These dependencies have their 2.13 suffixed alternatives explicitly excluded.
  • update scala-parser-combinators to be the same version as that used by eldarica ( 1.1.2 -> 2.3.0)

[sankalpgambhir]

Models from z3 are now extracted and printed (:tada:). I'll add a commit soon to improve the printing for this.

Following the discovery of unsoundness when processing some invalid queries, I realized that the computation of arguments of predicates is not always simple in a single pass.

It is much safer to do it as two passes. This reduces the complexity of the encoding a bit, since there are quite a few less things to track once you give up doing things in one pass. This motivated a significant rewrite of the constraint generation.

Alongside this, there is now clearer support for polymorphic recursion since I was rewriting those parts already, wherein each concretely typed version of each function gets its own definition, clauses, and thus invariants. This adds a fixpoint computation in the constraint generation to transitively accumulate concrete calls, but this should terminate quite quickly if the program terminates (i.e. if you at least don't have unbounded polymorphic recursion).

Turns out that even in the two-pass generation, it is not always clear when certain guards should be injected into clauses (conditions under which certain variables' presence is justified), so that added a bit of complexity and thinking to the new implementation.

I've tested some more integer programs, valid and invalid. I'll be adding some of these as tests soon.

[sankalpgambhir]

New Eldarica intepreter is in and working. There is no longer a hardcoded dependence on an external wrapper. Communication with Eldarica happens through some string streams. Not great, but much better than starting new JVMs. Interruption (as expected by Inox's solver interface) is provided by using Java Executors / Futures.

There is (kinda) a provision to read models from Eldarica, but after a long session figuring out parsing errors, it was as simple as Eldarica not quite respecting the SMTLIB standard.

For models, Eldarica simply returns S-expressions for each element of the model, rather than an S-list. As a result, the model:

(
  (define-fun F ((A Int)) Bool (true)) 
)

becomes

(define-fun F ((A Int)) Bool (true)) 

and the empty model () becomes the empty string, so the SMTLIB parser is understandably unhappy.

The lines requesting and parsing the model from eldarica are thus commented out in the interpreter file for now. I'll make a PR on the eldarica repo to fix this. uuverifiers/eldarica#64

[sankalpgambhir]

Rebased wrt main

[sankalpgambhir]

Integrating this with Stainless will require minor changes to the build.sbt. I have that implemented, and can make a PR after this is merged.