initial commit

.gitignore

@@ -0,0 +1 @@
+__pycache__

.travis.yml

@@ -0,0 +1,11 @@
+language: python
+python:
+  - "3.6"      
+  - "3.7"
+  - "3.8"
+  - "nightly"  
+install:
+  - pip install antlr4-python3-runtime 
+  - pip install coverage
+script:
+  - python -m unittest tests/runtests.py

LICENSE.md

@@ -0,0 +1,7 @@
+Copyright 2020 Yin-Yang Contributors 
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

README.md

@@ -0,0 +1,128 @@
+![Travis](https://travis-ci.com/wintered/yinyang.svg?token=sgWHG8TT217zpf5KHHqh&branch=master)
+[![Twitter](https://img.shields.io/twitter/follow/testsmtsolvers?style=social)](https://twitter.com/testsmtsolvers)
+
+
+Yin-Yang <img width="35" alt="portfolio_view" align="left" src="./media/Yin_yang.svg"><img width="100" alt="portfolio_view" align="right" src="https://people.inf.ethz.ch/suz/logo/LOGO_AST.svg">
+========
+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 equisatisifiable formulas by fusing test seeds pairs of the same satisifiablity 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](https://github.com/Z3Prover/z3) or [CVC4](https://github.com/CVC4/CVC4)   
+
+The following commands clone Ying-Yang and installs the antlr4 python runtime: 
+```
+git clone https://github.com/wintered/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](./docs/documentation.md).
+
+#### Type-Aware Operator Mutation
+```
+python 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 neccessary for differential testing.
+
+
+* `<seed>`: an SMT-LIB v2.6 file
+
+Example:
+```
+python yinyang.py "z3;cvc4 -q" examples/formulas/a.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 cils is incorrect) or a bug has been found. If a bug has been found, the bug trigger is stored in `./bugs`.
+
+#### Semantic Fusion 
+
+```
+python yinyang.py "<solver_clis>" -o <oracle> -s fusion <seed1> <seed2>
+```
+
+where
+
+* `<solver_clis>`: a sequence of command line interfaces to call SMT solvers splitted 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: 
+
+```
+python yinyang.py "z3" -o sat -s fusion examples/formulas/a.smt2 examples/formulas/b.smt2 
+```
+Yin-Yang will test z3 by running *Semantic Fusion* with 30 iterations on the two satisifiable seed formulas. Note, the mutants generated by YinYang will then be by construction also be satisifable.
+
+
+Test Seeds & Limitations
+--------------
+SMT-LIB test seeds can be conveniently obtained via the following [script](http://smtlib.cs.uiowa.edu/SMT-LIB-clone.sh) or alternatively directly from the SMT-LIB initiatives gitlab repositories for [non-incremental](https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks) and [incremental](https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks-inc) 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 
+satisifable and unsatisfiable formulas. Pre-categorized are available in the following [repository](https://github.com/testsmt/semantic-fusion-seeds) 
+
+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]](https://arxiv.org/pdf/2004.08799.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]](https://dl.acm.org/doi/abs/10.1145/3385412.3385985)
+```
+@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}
+}
+```
+
+## Comparing against Yin-Yang 
+The testing approaches within Yin-Yang are slightly different from the research prototypes used for these publications. If you want to compare against either one of them, please contact us to provide you with these prototypes and the configurations  used.
+
+Contributers                                                                       
+------------                          
+* [Dominik Winterer](https://wintered.github.io/) (primary maintainer) - [email protected]
+
+* [Chengyu Zhang](http://chengyuzhang.com/) (primary maintainer) - [email protected]
+
+* [Zhendong Su](https://people.inf.ethz.ch/suz/) - [email protected] 

config/config.py

@@ -0,0 +1,36 @@
+solvers = [
+    "cvc4 --strings-exp --incremental --produce-models --check-unsat-cores --check-models --quiet",
+    "cvc4 --strings-exp --sygus-inference --produce-models --check-unsat-cores --check-models --quiet",
+    "z3release model_validate=true",
+    "z3release smt.ematching=false rewriter.flat=false smt.threads=3 smt.arith.solver=2 model_validate=true",
+    "z3release smt.ematching=false rewriter.flat=false smt.threads=3 model_validate=true"
+]
+
+crash_msgs = [
+    "LEAKED",
+    "Leaked",
+    "Segmentation fault",
+    "segmentation fault",
+    "segfault",
+    "ASSERTION VIOLATION",
+    "Assertion failure",
+    "Fatal failure",
+    "Internal error detected",
+    "an invalid model was generated",
+    "Failed to verify",
+    "failed to verify",
+    "ERROR: AddressSanitizer:",
+    "invalid expression"
+]
+
+ignore_msgs = [
+    "(error",
+    "Expected result sat but got unsat",
+    "Expected result unsat but got sat",
+    "Parse Error",
+    "Cannot get model",
+    "Symbol 'str.to-re' not declared as a variable",
+    "Symbol 'str.to.re' not declared as a variable",
+    "Unimplemented code encountered",
+    '(error "Error in option parsing: sygus inference not supported with incremental solving")'
+]

config/fusion_functions.txt

@@ -0,0 +1,137 @@
+; Configuration file for fusion and inversion functions as described in PLDI 2020 
+; paper's Definition 1 and Definition 2 which we will repeat here.  
+;  
+; Definition 1 (Fusion function).  
+; Let phi1, phi2 be formulas and x and y be variables of phi1 and phi2 
+; respectively, and z a fresh variable which does not occur in neither phi1 nor 
+; phi2. We define  z := f(x,y) and call f a fusion function.   
+;               
+;
+; Definition 2 (Inversion function). 
+; Let phi1, phi2 be formulas and f be a fusion function. For two variables x and 
+; y be variables of phi1 and phi2 and z = f(x,y), we define  
+; x = r_x(y,z); y = r_y (x,z) and call them inversion functions.  
+;
+; ** File format:  
+;
+; Each triplet of a fusion and two inversion functions is contained within a     
+; "#begin-#end" block. Note, variables x,y,z are hard-coded to reflect Definition 1
+; and Definition 2 closely and should be declared as three constants. An additional 
+; constant "c" represents a randomly chosen constant. The first assert represents    
+; the equation "z := f(x,y)", the second and third represent the equations    
+; x = r_x(y,z) and y = r_y (x,z) respectively. 
+;
+; The below fusion and inversion function triplets are based on the PLDI 2020 paper.    
+;
+; Int
+;
+#begin
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+(assert (= z (* x y)))
+(assert (= x (div z y)))
+(assert (= y (div z x)))
+#end
+
+#begin
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+(assert (= z (+ x y)))
+(assert (= x (- z y)))
+(assert (= y (- z x)))
+#end
+
+#begin
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+(declare-const c Int)
+(assert (= z (+ x c) y))
+(assert (= x (- (- z  c) y)))
+(assert (= y (- (- z  c) x)))
+#end
+
+; Real
+;
+#begin
+(declare-const x Real)
+(declare-const y Real)
+(declare-const z Real)
+(assert (= z (* x y)))
+(assert (= x (/ z y)))
+(assert (= y (/ z x)))
+#end
+
+#begin
+(declare-const x Real)
+(declare-const y Real)
+(declare-const z Real)
+(declare-const c Real)
+(assert (= z (+ (+ x c) y)))
+(assert (= x (- z y)))
+(assert (= y (- z x)))
+#end
+
+#begin
+(declare-const x Real)
+(declare-const y Real)
+(declare-const z Real)
+(declare-const c Real)
+(assert (= z (+ x c) y))
+(assert (= x (- (- z  c) y)))
+(assert (= y (- (- z  c) x)))
+#end
+
+; Bool
+;
+#begin
+(declare-const x Bool)
+(declare-const y Bool)
+(declare-const z Bool)
+(assert (= z (xor x y)))
+(assert (= x (xor z y)))
+(assert (= y (xor z x)))
+#end
+
+; BV
+;
+#begin
+(declare-const x (_ BitVec 8))
+(declare-const y (_ BitVec 8))
+(declare-const z (_ BitVec 8))
+(assert (= z (bvxor x y)))
+(assert (= x (bvxor z y)))
+(assert (= y (bvxor z x)))
+#end
+
+; String
+;
+#begin
+(declare-const x String)
+(declare-const y String)
+(declare-const z String)
+(assert (= z (str++ x y)))
+(assert (= x (str.substr z 0 (str.len x))))
+(assert (= y (str.substr z 0 (str.len y))))
+#end
+
+#begin
+(declare-const x String)
+(declare-const y String)
+(declare-const z String)
+(assert (= z (str++ x y)))
+(assert (= x (str.substr z 0 (str.len x))))
+(assert (= y (str.replace z x "")))
+#end
+
+#begin
+(declare-const x String)
+(declare-const y String)
+(declare-const z String)
+(declare-const c String)
+(assert (= z (str++ x y c)))
+(assert (= x (str.substr z 0 (str.len x))))
+(assert (= y (str.replace (str.replace z x "") c "")))
+#end

config/operator_mutations.txt

@@ -0,0 +1,35 @@
+; Configuration file for the type-aware operator mutations based on the operators 
+; as specified in the OOPSLA '20 paper. 
+;
+; Format:
+;
+; op1, op2, ... ,op_n
+;
+; Operators op_i in the same line form an equivalence class and can mutually 
+; replace each other. 
+;
+; Example:
+; +, -, * 
+;
+; Operator mutations can be conditioned on operator's arity. 
+; 
+; Example: 
+; =,distinct: arity: 2+ 
+; -,abs: arity: 1- 
+;
+; This requires operators "=" and "distinct" to have at least two arguments to trigger the  
+; mutation, and "-","abs" to have at most one argument. At the moment, only the arities  
+; 2+ ("two or more") and 1- (one or less) are supported  
+; 
+; Unidirectional mutations can be specified as   
+; 
+; abs -> - 
+;
+; which corresponds to a one-way mutation from operator "abs" to operator "-" 
+;
+=,distinct
+exists,forall
+and,or,=>
+<=, >=,<,>
++,-,*,/ :arity 2+
+mod -> div