Solving SMT formulas involving the theory of floating-pointing arithmetic (FPA)
can be required in several domains including symbolic execution, test generation,
and program synthesis. Unfortunately, SMT solvers often struggle
trying to satisfy given FPA queries. Additionally, commonly used non-linear functions,
e.g. trigonometric, remain unsupported.
This leaves tool developers with limited options like employing uninterpreted functions
which can be tricky or work around the issue by ignoring FPA altogether.
Recently, I've been exploring global optimization
as an alternative option for tackling this problem. This approach is unconventional
in the sense that it departs away from the known and trusted DPLL(T) framework.
This work is based on the ideas published in the XSat
paper by Fu et al. (CAV'16). Our results are discussed in this report.
This work is implemented in the SMT solver goSAT which is publicly available.
We provide in the following an appendix to our report in Q&A format.
I find this format particularly useful for providing quick takeaways
to interested readers.
Additionally, it can help in clearing possible misunderstandings.
Appendix
Note. This appendix was edited in collaboration with Dominik Stoffel and Wolfgang Kunz.
Errors and omissions are mine.
| Q: | Evaluations results demonstrate that MathSat still compares favorably in terms of SAT instances solved.
Why do we need exploring alternatives to conventional solvers? |
|---|
| A: | Our experimental evaluation considered only one set of FPA benchmarks.
Hence, it's still early to draw general conclusions.
Actually, our main target was assessing the potential of different GO
algorithms rather than comparing with MathSAT. Also, the merit of goSAT
is that it can, in principle, reason about any executable function, e.g., trigonometric
functions, which is not possible in MathSat. Further, extending MathSat to
Optimization-Modulo-Theory (OMT) over FPA will require implementing GO algorithms
similar to the ones we discussed. Finally, goSAT has a significant advantage in
terms of query time and used memory despite the fact that it's still at an early stage. |
|---|
| Q: | Wouldn't compiler optimizations affect the soundness of the results? |
|---|
| A: | goSAT emits a restricted IR subset that doesn't have common features
like loops and heap allocations. Also, compiler optimizations are restricted to only one
function representing \(\mathcal{G}(\vec{x})\), i.e. intra-procedural optimizations only.
Works on compiler validation e.g. EMI [PLDI14] and CSmith [PLDI11], demonstrate that
compiler miscompilation bugs generally require code with more complex features.
Additionally, goSAT is incomplete when stochastic GO algorithms are applied.
However, it is sound w.r.t. SAT results.
SAT results are easy to validate externally using a simple evaluation.
We implemented this feature in goSAT and, so far, did not encounter invalid results.
Consequently, we do not consider potential compiler bugs to be a serious drawback. |
|---|
| Q: | What are the contributions of goSAT over XSat? |
|---|
| A: | We provide several contributions over XSat.
First, XSat discussed one stochastic GO algorithm (MCMC sampling) and used Scipy as backend
in the experimentation. Scipy supports only one GO algorithm, namely, Basin Hopping.
In comparison, we provide a design-space exploration of different algorithms and backends, e.g., NLopt and IpOpt.
We evaluated four stochastic algorithms and one deterministic algorithm.
Second, our tool, goSAT, is publicly available while XSat is not public.
Third, with BH solver we provide an open re-implementation of XSat with the same optimization parameters,
as provided to us by the XSat authors.
Fourth, goSAT is more portable compared to XSat since it uses CTypes for FFI instead of C extensions for Python.
Despite this, solving time of both tools is still comparable.
Fifth, we highlighted equations (9-11) which were overlooked in XSat despite being necessary for proving soundness.
Sixth, based on Figure 2, we made the observation that the regularity of generated functions is essential
to making goSAT work in practice.
Finally, XSat requires a manual setup to get working.
In contrast, goSAT is an integrated tool featuring JIT compilation of SMT formulas.
To our knowledge, we are the first to implement this in the context of SMT solving. |
|---|
| Q: | BH and NL solvers only work if given a compiled shared library as "input".
One would typically expect an SMT formula to be given as input instead? |
|---|
| A: | In code generation mode, goSAT generates C code (like XSat) that corresponds
to the given input formula(s). This code needs
to be compiled and given as input to BH or NL solvers. Additionally, goSAT can
solve SMT formulas directly. This is an extension over XSat and a key contribution. |
|---|
| Q: | Can goSAT provide stable results after multiple runs on the same formula? |
|---|
| A: | With stochastic search, a certain degree of instability is unavoidable.
In our experiments, however, we experienced stable results with the majority
of input formulas. For example, applying CRS2 algorithm to the 214 instances in the griggio benchmarks,
we found only two instances, namely, sqrt_c_2 and sqrt_c_5, to
lead to what can be considered unstable results. |
|---|
| [PLDI14] | V. Le, M. Afshari, and Z. Su, “Compiler validation via equivalence modulo inputs,” in Proceedings of the 35th Conference on Programming Languages Design and Implementation (PLDI’14), 2014, pp. 216–226. |
| [PLDI11] | X. Yang, Y. Chen, E. Eide, and J. Regehr, “Finding and understanding bugs in C compilers,” in Proceedings of the 32nd conference on Programming language design and implementation (PLDI’11), 2011, pp. 283–294. |
Formally Applied