/yinyang

SMT Solver Testing Framework

Primary LanguagePythonMIT LicenseMIT

Travis Twitter

Yin-Yang portfolio_viewportfolio_view

Yin-Yang is a tool for automatically stress-testing Satisfiability Modulo Theory (SMT) solvers. Given a set of SMT-LIB v2.6 seed formulas, Yin-Yang generates mutant formulas that are then used as the test seeds for SMT solvers. It currently supports two mutation-based testing approaches.

  • Type-Aware Operator Mutation [OOPSLA '20] mutates operators within SMT-LIB formulas and differentially tests two or more SMT solvers for inconsistent results.

  • Semantic Fusion [PLDI '20] is a metamorphic testing approach that generates an equisatisfiable formulas by fusing test seeds pairs of the same satisfiability to stress test one or more SMT solvers.

Installation

Requirements:

  • python 3.6+
  • antlr4 python runtime
  • SMT-LIB v2.6 tests seeds
  • SMT solver(s) under tests, e.g., Z3 or CVC4

The following commands clone Yin-Yang and install the antlr4 python runtime:

git clone https://github.com/testsmt/yinyang.git 
pip3 install antlr4-python3-runtime

Usage

Yin-Yang currently supports two mutation-based testing strategies. Type-Aware Operator Mutation which mutates operators within SMT-LIB formulas and needs two or more SMT solvers for differential testing and Semantic Fusion, a metamorphic testing approach which fuses pairs of seed formulas into an equisatisfiable mutant test formula. In the following, we will illustrate the basic usage of both with standard configurations. For more detailed configuration, see documentation.md.

Type-Aware Operator Mutation

python3 yinyang.py "<solver_clis>" <seed>

where

  • <solver_clis>: a sequence of command line interfaces to call SMT solvers splitted by semicola ;. Note that at least two SMT solvers are necessary for differential testing.

  • <seed>: an SMT-LIB v2.6 file

Example:

python3 yinyang.py "z3;cvc4 -q" examples/formulas/phi1.smt2

Yin-Yang will run Type-Aware Operator Mutation and generate 300 mutations on the seed for stress-testing z3 and cvc4. The expected behaviour of Yin-Yang is to output anything to stdout unless an error occurred (e.g. one of the solver clis is incorrect) or a bug has been found. If a bug has been found, the bug trigger is stored in ./bugs.

Semantic Fusion

python3 yinyang.py "<solver_clis>" -o <oracle> -s fusion <seed1> <seed2>

where

  • <solver_clis>: a sequence of command line interfaces to call SMT solvers separated by semicola ;. Note, since Semantic Fusion is a metamorphic testing approach, one SMT solver is sufficient.

  • <oracle>: desired test oracle result {sat, unsat}.

  • <seed1>, <seed2>: SMT-LIB v2.6 file of the same satisfiability, i.e. both either sat or unsat in according with the oracle.

Example:

python3 yinyang.py "z3" -o sat -s fusion examples/formulas/phi1.smt2 examples/formulas/phi2.smt2

Yin-Yang will test z3 by running Semantic Fusion with 30 iterations on the two satisfiable seed formulas. Note, the mutants generated by Yin-Yang will then be by construction also be satisfiable.

Test Seeds & Limitations

SMT-LIB test seeds can be conveniently obtained via the following script or alternatively directly from the SMT-LIB initiatives gitlab repositories for non-incremental and incremental benchmarks. For fuzzing with Yin-Yang, we recommend to prioritize small-sized SMT-LIB files.

Limitations

Yin-Yang's parser supports the SMT-LIB v2.6 standard and so it is able to parse existing SMT-LIB. Type-Aware Operator Mutation can be used for formulas as any logic while Semantic Fusion currently only supports LIA, LRA, NRA, QF_LIA, QF_LRA, QF_NRA, QF_SLIA, QF_S logics in the non-incremental mode. To apply Semantic Fusion, test seeds Support for other logics is experimental; we are actively working on it. For Semantic Fusion, the seeds need to be pre-processed to separate them into satisfiable and unsatisfiable formulas. Pre-categorized are available in the following repository

Yin-Yang may also not be able to parse some non-standard .smt2 files such as, e.g., some files from the regression test suites of Z3 and CVC4. We are working on an extension of the parser to support such files.

A further limitation of Yin-Yang is that it currently only supports modifying expression inside assert statements. Support for other SMT-LIB commands expressions will be added shortly.

Citation

The testing approaches implemented in Yin-Yang are based on following two papers.

Type-Aware Operator Mutation [pdf]

@misc{winterer-zhang-su-arxiv2020,
      title={On the Unusual Effectiveness of Type-aware Mutations for Testing SMT Solvers}, 
      author={Dominik Winterer and Chengyu Zhang and Zhendong Su},
      year={2020},
      eprint={2004.08799},
      archivePrefix={arXiv}
}

Semantic Fusion [pdf]

@inproceedings{winterer-zhang-su-pldi2020,
      title = {Validating SMT Solvers via Semantic Fusion},
      author = {Winterer, Dominik and Zhang, Chengyu and Su, Zhendong},
      year = {2020},
      booktitle = {Proceedings of the 41st ACM SIGPLAN Conference on Programming 
                   Language Design and Implementation},
      pages = {718–730}
}

Contributors