A fuzzing framework for SMT solvers

Overview

portfolio_view


yinyang

A fuzzing framework for SMT solvers. Given a set of seed SMT formulas, yinyang generates mutant formulas to stress-test SMT solvers. yinyang can be used to robustify SMT solvers. It already found 1,500+ bugs in the two state-of-the-art SMT solvers Z3 and CVC4.

Installation

To install a stable version of yinyang use:

pip3 install yinyang

To install the most recent version, check out the repository:

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

Note that you may want to add yinyang/bin to your PATH, for running yinyang conveniently without prefix.

Usage

  1. Get SMT-LIB 2 benchmarks. Edit scripts/SMT-LIB-clone.sh to select the logics for testing. Run ./scripts/SMT-LIB-clone.sh to download the corresponding SMT-LIB 2 benchmarks. Alternatively, you can download benchmarks directly from the SMT-LIB website or supply your own benchmarks.

  2. Get and build SMT solvers for testing. Install two or more SMT solvers that support the SMT-LIB 2 format. You may find it convenient to add them to your PATH.

  3. Run yinyang on the benchmarks e.g. with Z3 and CVC4.

typefuzz "z3 model_validate=true;cvc4 --check-models -m -i -q" benchmarks 

yinyang will by default randomly select formulas from the folder ./benchmarks and generate 300 mutants per seed formula. If a bug has been found, the bug trigger is stored in ./bugs. yinyang will run in an infinite loop. You can use the shortcut CTRL+C to terminate yinyang manually.

📘 Documentation

Feedback

For bugs/issues/questions/feature requests please file an issue. We are always happy to receive your feedback or help you adjust yinyang to the needs of your custom solver, help you build on yinyang, etc.

📬 Contact us

Additional Resources

Comments
  • Issues with respect to fusion

    Issues with respect to fusion

    Hi, When I used YinYang (fusion), I found it generated some instances contains syntax errors. For example:

    (declare-fun scr1_liipp_0_c () Real)
    (declare-fun scr1_liipp_0__main_offset () Real)
    (declare-fun scr1_liipp_0__main_length () Real)
    (declare-fun scr1_liipp_1_c () Real)
    (declare-fun scr1_liipp_1__main_offset () Real)
    (declare-fun scr1_liipp_1__main_length () Real)
    (declare-fun scr1_liipp_2_c () Real)
    (declare-fun scr1_liipp_2__main_offset () Real)
    (declare-fun scr1_liipp_2__main_length () Real)
    (declare-fun scr1_liipp_3_c () Real)
    (declare-fun scr1_liipp_3__main_offset () Real)
    (declare-fun scr1_liipp_3__main_length () Real)
    (declare-fun scr1_liipp_4_replace_0 () Real)
    (declare-fun scr1_liipp_4_replace_1 () Real)
    (declare-fun scr1_liipp_5_replace_0 () Real)
    (declare-fun scr1_liipp_5_replace_1 () Real)
    (declare-fun scr1_motzkin_6304_0 () Real)
    (declare-fun scr1_motzkin_6304_1 () Real)
    (declare-fun scr1_motzkin_6304_2 () Real)
    (declare-fun scr1_motzkin_6304_3 () Real)
    (declare-fun scr1_motzkin_6304_4 () Real)
    (declare-fun scr1_motzkin_6305_0 () Real)
    (declare-fun scr1_motzkin_6305_1 () Real)
    (declare-fun scr1_motzkin_6305_2 () Real)
    (declare-fun scr1_motzkin_6305_3 () Real)
    (declare-fun scr1_motzkin_6305_4 () Real)
    (declare-fun scr1_motzkin_6306_0 () Real)
    (declare-fun scr1_motzkin_6306_1 () Real)
    (declare-fun scr1_motzkin_6306_2 () Real)
    (declare-fun scr1_motzkin_6306_3 () Real)
    (declare-fun scr1_motzkin_6307_0 () Real)
    (declare-fun scr1_motzkin_6307_1 () Real)
    (declare-fun scr1_motzkin_6307_2 () Real)
    (declare-fun scr1_motzkin_6307_3 () Real)
    (declare-fun scr1_motzkin_6308_0 () Real)
    (declare-fun scr1_motzkin_6308_1 () Real)
    (declare-fun scr1_motzkin_6308_2 () Real)
    (declare-fun scr2_liipp_0_c () Real)
    (declare-fun scr2_liipp_0__main_offset () Real)
    (declare-fun scr2_liipp_0__main_length () Real)
    (declare-fun scr2_liipp_1_c () Real)
    (declare-fun scr2_liipp_1__main_offset () Real)
    (declare-fun scr2_liipp_1__main_length () Real)
    (declare-fun scr2_liipp_2_c () Real)
    (declare-fun scr2_liipp_2__main_offset () Real)
    (declare-fun scr2_liipp_2__main_length () Real)
    (declare-fun scr2_liipp_3_c () Real)
    (declare-fun scr2_liipp_3__main_offset () Real)
    (declare-fun scr2_liipp_3__main_length () Real)
    (declare-fun scr2_liipp_4_replace_0 () Real)
    (declare-fun scr2_liipp_4_replace_1 () Real)
    (declare-fun scr2_liipp_5_replace_0 () Real)
    (declare-fun scr2_liipp_5_replace_1 () Real)
    (declare-fun scr2_motzkin_6261_0 () Real)
    (declare-fun scr2_motzkin_6261_1 () Real)
    (declare-fun scr2_motzkin_6261_2 () Real)
    (declare-fun scr2_motzkin_6261_3 () Real)
    (declare-fun scr2_motzkin_6261_4 () Real)
    (declare-fun scr2_motzkin_6262_0 () Real)
    (declare-fun scr2_motzkin_6262_1 () Real)
    (declare-fun scr2_motzkin_6262_2 () Real)
    (declare-fun scr2_motzkin_6262_3 () Real)
    (declare-fun scr2_motzkin_6262_4 () Real)
    (declare-fun scr1_liipp_4_replace_0_scr2_motzkin_6263_1_fused () Real)
    (declare-fun scr1_liipp_1__main_length_scr2_liipp_2_c_fused () Real)
    (declare-fun scr1_liipp_2_c_scr2_liipp_2__main_offset_fused () Real)
    (declare-fun scr1_motzkin_6307_3_scr2_liipp_4_replace_0_fused () Real)
    (declare-fun scr1_motzkin_6304_1_scr2_motzkin_6261_1_fused () Real)
    (declare-fun scr1_liipp_2__main_length_scr2_liipp_0__main_offset_fused () Real)
    (declare-fun scr1_liipp_1_c_scr2_motzkin_6262_3_fused () Real)
    (declare-fun scr1_liipp_4_replace_1_scr2_motzkin_6262_4_fused () Real)
    (declare-fun scr1_motzkin_6305_3_scr2_motzkin_6263_2_fused () Real)
    (declare-fun scr1_motzkin_6306_0_scr2_liipp_1__main_offset_fused () Real)
    (declare-fun scr1_liipp_0__main_offset_scr2_motzkin_6262_2_fused () Real)
    (declare-fun scr1_motzkin_6307_1_scr2_motzkin_6262_0_fused () Real)
    (declare-fun scr1_motzkin_6307_2_scr2_motzkin_6264_0_fused () Real)
    (declare-fun scr1_liipp_5_replace_1_scr2_motzkin_6263_0_fused () Real)
    (declare-fun scr1_liipp_2__main_offset_scr2_liipp_0__main_length_fused () Real)
    (declare-fun scr1_motzkin_6305_4_scr2_liipp_1_c_fused () Real)
    (declare-fun scr1_liipp_3__main_offset_scr2_liipp_0_c_fused () Real)
    (assert (and (and (and (>= scr1_motzkin_6304_0 0.0) (>= scr1_motzkin_6304_1 0.0) (>= scr1_motzkin_6304_2 0.0) (>= scr1_motzkin_6304_3 0.0) (>= scr1_motzkin_6304_4 0.0) (= (+ scr1_motzkin_6304_0 (* (- scr1_motzkin_6304_1_scr2_motzkin_6261_1_fused scr2_motzkin_6261_1) (- 1.0)) (* scr1_motzkin_6304_4 (+ (* (- 1.0) (- scr1_liipp_0__main_offset_scr2_motzkin_6262_2_fused scr2_motzkin_6262_2)) 0.0))) 0.0) (= (+ scr1_motzkin_6304_2 (* scr1_motzkin_6304_3 (- 1.0)) (* scr1_motzkin_6304_4 (+ (* (- 1.0) scr1_liipp_0__main_length) 0.0))) 0.0) (<= (+ (* scr1_motzkin_6304_2 (- 40000.0)) (* scr1_motzkin_6304_3 40000.0) (* scr1_motzkin_6304_4 (+ (* (- 1.0) scr1_liipp_0_c) 0.0))) 0.0) (or (< (+ (* scr1_motzkin_6304_2 (- 40000.0)) (* scr1_motzkin_6304_3 40000.0) (* scr1_motzkin_6304_4 (+ (* (- 1.0) scr1_liipp_0_c) 0.0))) 0.0) (> 0.0 0.0)) (>= scr1_motzkin_6305_0 0.0) (>= scr1_motzkin_6305_1 0.0) (>= scr1_motzkin_6305_2 0.0) (>= scr1_motzkin_6305_3 0.0) (>= scr1_motzkin_6305_4 0.0) (= (+ scr1_motzkin_6305_0 (* scr1_motzkin_6305_1 (- 1.0)) (* scr1_motzkin_6305_4 (+ (* (- 1.0) scr1_liipp_1__main_offset) 0.0))) 0.0) (= (+ scr1_motzkin_6305_2 (* (- (- scr1_motzkin_6305_3_scr2_motzkin_6263_2_fused scr2_motzkin_6263_2) 350.94844) (- 1.0)) (* scr1_motzkin_6305_4 (+ (* (- 1.0) scr1_liipp_1__main_length) 0.0))) 0.0) (<= (+ (* scr1_motzkin_6305_2 (- 40000.0)) (* scr1_motzkin_6305_3 40000.0) (* scr1_motzkin_6305_4 (+ (* (- 1.0) (- (- scr1_liipp_1_c_scr2_motzkin_6262_3_fused 363.76579) scr2_motzkin_6262_3)) 0.0))) 0.0) (or (< (+ (* scr1_motzkin_6305_2 (- 40000.0)) (* scr1_motzkin_6305_3 40000.0)) 0.0) (> scr1_motzkin_6305_4 0.0))) (and (>= (- (- scr1_motzkin_6306_0_scr2_liipp_1__main_offset_fused scr2_liipp_1__main_offset) (- 922.62598)) 0.0) (>= scr1_motzkin_6306_1 0.0) (>= scr1_motzkin_6306_2 0.0) (>= scr1_motzkin_6306_3 0.0) (= (+ (* scr1_motzkin_6306_0 (- 1.0)) (* scr1_motzkin_6306_1 (+ (* (- 1.0) scr1_liipp_2__main_offset) 0.0)) (* scr1_motzkin_6306_2 (+ (* 1.0 (- scr1_liipp_0__main_offset_scr2_motzkin_6262_2_fused scr2_motzkin_6262_2)) 0.0)) (* scr1_motzkin_6306_3 (+ (* 1.0 scr1_liipp_1__main_offset) 0.0))) 0.0) (= (+ (- (- scr1_motzkin_6306_0_scr2_liipp_1__main_offset_fused scr2_liipp_1__main_offset) (- 922.62598)) (* scr1_motzkin_6306_1 (+ (* (- 1.0) scr1_liipp_2__main_length) 0.0)) (* scr1_motzkin_6306_2 (+ (* 1.0 scr1_liipp_0__main_length) 0.0)) (* scr1_motzkin_6306_3 (+ (* 1.0 scr1_liipp_1__main_length) 0.0))) 0.0) (<= (+ (* scr1_motzkin_6306_0 (- 1.0)) (* scr1_motzkin_6306_1 (+ (* (- 1.0) (- (- scr1_liipp_2_c_scr2_liipp_2__main_offset_fused scr2_liipp_2__main_offset) 829.94541)) 0.0)) (* scr1_motzkin_6306_2 (+ (* 1.0 scr1_liipp_0_c) 0.0)) (* scr1_motzkin_6306_3 (+ (* 1.0 (- (- scr1_liipp_1_c_scr2_motzkin_6262_3_fused 363.76579) scr2_motzkin_6262_3)) 0.0))) 0.0) (or (< (+ (* (- (- scr1_motzkin_6306_0_scr2_liipp_1__main_offset_fused scr2_liipp_1__main_offset) (- 922.62598)) (- 1.0)) (* scr1_motzkin_6306_1 (+ (* (- 1.0) scr1_liipp_2_c) 0.0)) (* scr1_motzkin_6306_3 (+ (* 1.0 scr1_liipp_1_c) 0.0))) 0.0) (> scr1_motzkin_6306_2 0.0)) (>= scr1_motzkin_6307_0 0.0) (>= (/ scr1_motzkin_6307_1_scr2_motzkin_6262_0_fused scr2_motzkin_6262_0) 0.0) (>= scr1_motzkin_6307_2 0.0) (>= scr1_motzkin_6307_3 0.0) (= (+ (* scr1_motzkin_6307_0 (- 1.0)) (* (/ scr1_motzkin_6307_1_scr2_motzkin_6262_0_fused scr2_motzkin_6262_0) (+ (* (- 1.0) (- (- scr1_liipp_3__main_offset_scr2_liipp_0_c_fused 243.32956) scr2_liipp_0_c)) 0.0)) (* scr1_motzkin_6307_2 (+ (* 1.0 scr1_liipp_0__main_offset) 0.0)) (* (- (- scr1_motzkin_6307_3_scr2_liipp_4_replace_0_fused 251.25255) scr2_liipp_4_replace_0) (+ (* 1.0 scr1_liipp_1__main_offset) 0.0))) 0.0) (= (+ scr1_motzkin_6307_0 (* (/ scr1_motzkin_6307_1_scr2_motzkin_6262_0_fused scr2_motzkin_6262_0) (+ (* (- 1.0) scr1_liipp_3__main_length) 0.0)) (* scr1_motzkin_6307_2 (+ (* 1.0 scr1_liipp_0__main_length) 0.0)) (* (- (- scr1_motzkin_6307_3_scr2_liipp_4_replace_0_fused 251.25255) scr2_liipp_4_replace_0) (+ (* 1.0 scr1_liipp_1__main_length) 0.0))) 0.0) (<= (+ (* scr1_motzkin_6307_0 (- 1.0)) (* (/ scr1_motzkin_6307_1_scr2_motzkin_6262_0_fused scr2_motzkin_6262_0) (+ (* (- 1.0) scr1_liipp_3_c) 0.0)) (* scr1_motzkin_6307_2 (+ (* 1.0 scr1_liipp_0_c) 0.0)) (* scr1_motzkin_6307_3 (+ (* 1.0 (- (- scr1_liipp_1_c_scr2_motzkin_6262_3_fused 363.76579) scr2_motzkin_6262_3)) 0.0))) 0.0) (or (< (+ (* scr1_motzkin_6307_0 (- 1.0)) (* (- (- scr1_motzkin_6307_3_scr2_liipp_4_replace_0_fused 251.25255) scr2_liipp_4_replace_0) (+ (* 1.0 scr1_liipp_1_c) 0.0))) 0.0) (> (+ (/ scr1_motzkin_6307_1_scr2_motzkin_6262_0_fused scr2_motzkin_6262_0) scr1_motzkin_6307_2) 0.0))) (and (>= scr1_motzkin_6308_0 0.0) (>= scr1_motzkin_6308_1 0.0) (>= scr1_motzkin_6308_2 0.0) (= (+ scr1_motzkin_6308_0 (* scr1_motzkin_6308_1 (+ (* 1.0 scr1_liipp_2__main_offset) 0.0)) (* scr1_motzkin_6308_2 (+ (* 1.0 (- (- scr1_liipp_3__main_offset_scr2_liipp_0_c_fused 243.32956) scr2_liipp_0_c)) 0.0))) 0.0) (= (+ (* scr1_motzkin_6308_0 (- 1.0)) (* scr1_motzkin_6308_1 (+ (* 1.0 (- (- scr1_liipp_2__main_length_scr2_liipp_0__main_offset_fused 428.59846) scr2_liipp_0__main_offset)) 0.0)) (* scr1_motzkin_6308_2 (+ (* 1.0 scr1_liipp_3__main_length) 0.0))) 0.0) (<= (+ (* scr1_motzkin_6308_0 3.0) (* scr1_motzkin_6308_1 (+ (* 1.0 (- (- scr1_liipp_2_c_scr2_liipp_2__main_offset_fused scr2_liipp_2__main_offset) 829.94541)) 0.0)) (* scr1_motzkin_6308_2 (+ (* 1.0 scr1_liipp_3_c) 0.0))) 0.0) (or (< (+ (* scr1_motzkin_6308_0 3.0) (* scr1_motzkin_6308_2 (+ (* 1.0 scr1_liipp_3_c) 0.0))) 0.0) (> scr1_motzkin_6308_1 0.0)))) (and (and (>= scr2_motzkin_6261_0 0.0) (>= (- scr1_motzkin_6304_1_scr2_motzkin_6261_1_fused scr1_motzkin_6304_1) 0.0) (>= scr2_motzkin_6261_2 0.0) (>= scr2_motzkin_6261_3 0.0) (>= scr2_motzkin_6261_4 0.0) (= (+ (* scr2_motzkin_6261_0 (- 1.0)) (- scr1_motzkin_6304_1_scr2_motzkin_6261_1_fused scr1_motzkin_6304_1) (* scr2_motzkin_6261_4 (+ (* (- 1.0) scr2_liipp_0__main_length) 0.0))) 0.0) (= (+ scr2_motzkin_6261_2 (* scr2_motzkin_6261_3 (- 1.0)) (* scr2_motzkin_6261_4 (+ (* (- 1.0) (- (- scr1_liipp_2__main_length_scr2_liipp_0__main_offset_fused 428.59846) scr1_liipp_2__main_length)) 0.0))) 0.0) (<= (+ (* scr2_motzkin_6261_0 1048.0) (* (- scr1_motzkin_6304_1_scr2_motzkin_6261_1_fused scr1_motzkin_6304_1) (- 1048.0)) (* scr2_motzkin_6261_4 (+ (* (- 1.0) scr2_liipp_0_c) 0.0))) 0.0) (or (< (+ (* scr2_motzkin_6261_0 1048.0) (* (- scr1_motzkin_6304_1_scr2_motzkin_6261_1_fused scr1_motzkin_6304_1) (- 1048.0)) (* scr2_motzkin_6261_4 (+ (* (- 1.0) scr2_liipp_0_c) 0.0))) 0.0) (> 0.0 0.0)) (>= (/ scr1_motzkin_6307_1_scr2_motzkin_6262_0_fused scr1_motzkin_6307_1) 0.0) (>= scr2_motzkin_6262_1 0.0) (>= scr2_motzkin_6262_2 0.0) (>= scr2_motzkin_6262_3 0.0) (>= (- (- scr1_liipp_4_replace_1_scr2_motzkin_6262_4_fused (- 232.60698)) scr1_liipp_4_replace_1) 0.0) (= (+ (* scr2_motzkin_6262_0 (- 1.0)) scr2_motzkin_6262_1 (* (- (- scr1_liipp_4_replace_1_scr2_motzkin_6262_4_fused (- 232.60698)) scr1_liipp_4_replace_1) (+ (* (- 1.0) scr2_liipp_1__main_length) 0.0))) 0.0) (= (+ scr2_motzkin_6262_2 (* scr2_motzkin_6262_3 (- 1.0)) (* (- (- scr1_liipp_4_replace_1_scr2_motzkin_6262_4_fused (- 232.60698)) scr1_liipp_4_replace_1) (+ (* (- 1.0) scr2_liipp_1__main_offset) 0.0))) 0.0) (<= (+ (* (/ scr1_motzkin_6307_1_scr2_motzkin_6262_0_fused scr1_motzkin_6307_1) 1048.0) (* scr2_motzkin_6262_1 (- 1048.0)) (* (- (- scr1_liipp_4_replace_1_scr2_motzkin_6262_4_fused (- 232.60698)) scr1_liipp_4_replace_1) (+ (* (- 1.0) scr2_liipp_1_c) 0.0))) 0.0) (or (< (+ (* scr2_motzkin_6262_0 1048.0) (* scr2_motzkin_6262_1 (- 1048.0))) 0.0) (> (- (- scr1_liipp_4_replace_1_scr2_motzkin_6262_4_fused (- 232.60698)) scr1_liipp_4_replace_1) 0.0))) (and (>= scr2_motzkin_6263_0 0.0) (>= scr2_motzkin_6263_1 0.0) (>= scr2_motzkin_6263_2 0.0) (>= scr2_motzkin_6263_3 0.0) (= (+ (* scr2_motzkin_6263_0 (- 1.0)) (* (- (- scr1_liipp_4_replace_0_scr2_motzkin_6263_1_fused 392.98169) scr1_liipp_4_replace_0) (+ (* (- 1.0) (- (- scr1_liipp_2_c_scr2_liipp_2__main_offset_fused scr1_liipp_2_c) 829.94541)) 0.0)) (* scr2_motzkin_6263_2 (+ (* 1.0 scr2_liipp_0__main_offset) 0.0)) (* scr2_motzkin_6263_3 (+ (* 1.0 (- (- scr1_motzkin_6306_0_scr2_liipp_1__main_offset_fused scr1_motzkin_6306_0) (- 922.62598))) 0.0))) 0.0) (= (+ scr2_motzkin_6263_0 (* (- (- scr1_liipp_4_replace_0_scr2_motzkin_6263_1_fused 392.98169) scr1_liipp_4_replace_0) (+ (* (- 1.0) scr2_liipp_2__main_length) 0.0)) (* (- (- scr1_motzkin_6305_3_scr2_motzkin_6263_2_fused scr1_motzkin_6305_3) 350.94844) (+ (* 1.0 (/ scr1_liipp_2__main_offset_scr2_liipp_0__main_length_fused scr1_liipp_2__main_offset)) 0.0)) (* scr2_motzkin_6263_3 (+ (* 1.0 scr2_liipp_1__main_length) 0.0))) 0.0) (<= (+ (* scr2_motzkin_6263_0 (- 1.0)) (* (- (- scr1_liipp_4_replace_0_scr2_motzkin_6263_1_fused 392.98169) scr1_liipp_4_replace_0) (+ (* (- 1.0) scr2_liipp_2_c) 0.0)) (* (- (- scr1_motzkin_6305_3_scr2_motzkin_6263_2_fused scr1_motzkin_6305_3) 350.94844) (+ (* 1.0 scr2_liipp_0_c) 0.0)) (* scr2_motzkin_6263_3 (+ (* 1.0 scr2_liipp_1_c) 0.0))) 0.0) (or (< (+ (* scr2_motzkin_6263_0 (- 1.0)) (* scr2_motzkin_6263_1 (+ (* (- 1.0) scr2_liipp_2_c) 0.0)) (* scr2_motzkin_6263_3 (+ (* 1.0 scr2_liipp_1_c) 0.0))) 0.0) (> (- (- scr1_motzkin_6305_3_scr2_motzkin_6263_2_fused scr1_motzkin_6305_3) 350.94844) 0.0)) (>= scr2_motzkin_6264_0 0.0) (>= scr2_motzkin_6264_1 0.0) (>= scr2_motzkin_6264_2 0.0) (>= scr2_motzkin_6264_3 0.0) (= (+ (* scr2_motzkin_6264_0 (- 1.0)) (* scr2_motzkin_6264_1 (+ (* (- 1.0) scr2_liipp_3__main_offset) 0.0)) (* scr2_motzkin_6264_2 (+ (* 1.0 scr2_liipp_0__main_offset) 0.0)) (* scr2_motzkin_6264_3 (+ (* 1.0 (- (- scr1_motzkin_6306_0_scr2_liipp_1__main_offset_fused scr1_motzkin_6306_0) (- 922.62598))) 0.0))) 0.0) (= (+ scr2_motzkin_6264_0 (* scr2_motzkin_6264_1 (+ (* (- 1.0) scr2_liipp_3__main_length) 0.0)) (* scr2_motzkin_6264_2 (+ (* 1.0 scr2_liipp_0__main_length) 0.0)) (* scr2_motzkin_6264_3 (+ (* 1.0 scr2_liipp_1__main_length) 0.0))) 0.0) (<= (+ (* scr2_motzkin_6264_0 (- 1.0)) (* scr2_motzkin_6264_1 (+ (* (- 1.0) scr2_liipp_3_c) 0.0)) (* scr2_motzkin_6264_2 (+ (* 1.0 scr2_liipp_0_c) 0.0)) (* scr2_motzkin_6264_3 (+ (* 1.0 scr2_liipp_1_c) 0.0))) 0.0) (or (< (+ (* scr2_motzkin_6264_0 (- 1.0)) (* scr2_motzkin_6264_3 (+ (* 1.0 (- (- scr1_motzkin_6305_4_scr2_liipp_1_c_fused scr1_motzkin_6305_4) (- 317.09221))) 0.0))) 0.0) (> (+ scr2_motzkin_6264_1 scr2_motzkin_6264_2) 0.0))) (and (>= scr2_motzkin_6265_0 0.0) (>= scr2_motzkin_6265_1 0.0) (>= scr2_motzkin_6265_2 0.0) (= (+ scr2_motzkin_6265_0 (* scr2_motzkin_6265_1 (+ (* 1.0 scr2_liipp_2__main_offset) 0.0)) (* scr2_motzkin_6265_2 (+ (* 1.0 scr2_liipp_3__main_offset) 0.0))) 0.0) (= (+ (* scr2_motzkin_6265_0 (- 1.0)) (* scr2_motzkin_6265_1 (+ (* 1.0 scr2_liipp_2__main_length) 0.0)) (* scr2_motzkin_6265_2 (+ (* 1.0 scr2_liipp_3__main_length) 0.0))) 0.0) (<= (+ (* scr2_motzkin_6265_0 3.0) (* scr2_motzkin_6265_1 (+ (* 1.0 scr2_liipp_2_c) 0.0)) (* scr2_motzkin_6265_2 (+ (* 1.0 scr2_liipp_3_c) 0.0))) 0.0) (or (< (+ (* scr2_motzkin_6265_0 3.0) (* scr2_motzkin_6265_2 (+ (* 1.0 scr2_liipp_3_c) 0.0))) 0.0) (> scr2_motzkin_6265_1 0.0))))))
    (declare-fun scr2_motzkin_6263_0 () Real)
    (declare-fun scr2_motzkin_6263_1 () Real)
    (declare-fun scr2_motzkin_6263_2 () Real)
    (declare-fun scr2_motzkin_6263_3 () Real)
    (declare-fun scr2_motzkin_6264_0 () Real)
    (declare-fun scr2_motzkin_6264_1 () Real)
    (declare-fun scr2_motzkin_6264_2 () Real)
    (declare-fun scr2_motzkin_6264_3 () Real)
    (declare-fun scr2_motzkin_6265_0 () Real)
    (declare-fun scr2_motzkin_6265_1 () Real)
    (declare-fun scr2_motzkin_6265_2 () Real)
    (check-sat)
    

    For this instance, z3 returns

    (error "line 81 column 1192: unknown constant scr2_motzkin_6263_2")
    sat
    

    Commit: 5b821b0

    bug 
    opened by merlinsun 5
  • Allow multiple constants c to appear in fusion functions

    Allow multiple constants c to appear in fusion functions

    Together with Lucas Weitzendorf, I am working at a fusion functions generator for our AST project.

    Our generator can build very long funsion functions and their inversions and we would like to allow multiple constants to appear within the same block. This PR allow such specifications (see below for the format description) and is retro compatible.

    I rely here on the naming convention (constant names are in the format c[0-9]*) as I have seen this is already practically used now.

    The new proposed format is:

    #begin
    <declaration of x>
    <declaration of y>
    <declaration of z>
    [<declaration of c_i>*]
    <assert fusion function>
    <assert inversion function>
    <assert inversion function>
    # end
    
    opened by nicdard 4
  • Feat: --keep-seeds and --generate-functions command line option

    Feat: --keep-seeds and --generate-functions command line option

    Add the command line option --keep-seeds (-k) with default value True. When set to False, scratch files will not be kept in the scratch folder after the Fuzzer executes, but the files will be created anyway.

    Add command line option for Semantic Fusion to generate fusion functions with the fusion function generator: https://github.com/nicdard/fusion-function-generator/pull/78 Use --generate-functions option (int value, the size of the functions) to generate a fusion function on demand to perform the fuse step of semantic fusion.

    opened by nicdard 3
  • Include name of all seeds in bug log

    Include name of all seeds in bug log

    The current version of yinyang only uses the last processed seed in the name of the bug log. This is not ideal if multiple seeds are used to trigger the bug, such as in semantic fusion.

    opened by lweitzendorf 1
  • Parser performance issues

    Parser performance issues

    Experiments on larger formulas, e.g., QF_FP 40kB+ formulas with highly nested expressions exposed hotspots while parsing.

    Actions:

    • Identify SMT-LIB formulas on which the parser times out
    • Profiling
    • Fix the hotspots
    bug 
    opened by wintered 1
  • Clarify statistics output

    Clarify statistics output

    Consider the following output

    Summary:
    Passed time: 48821s
    Generated mutants: 1346751
    Used seeds: 6
    Crash issues: 0
    Unsound issues: 0
    Timeout cases: 0
    Ignored issues: 139924
    

    A common questions (asked by students) seem to be: "What are Ignored Issues?".

    Actions:

    • (possibly) change the wording
    • add a description about
    documentation 
    opened by wintered 1
  • Improve format of usage/--help dialogue

    Improve format of usage/--help dialogue

    Actions:

    • make src/args.py consistent with the description in the documentation
    • prettify the output for yinyang.py (called without args) and help and yinyang.py --help
    $ python3.9 yinyang.py 
    usage: yinyang.py [-h] [-s {opfuzz,fusion}] [-o {sat,unsat}] [-i ITERATIONS] [-m MODULO] [-t TIMEOUT] [-d] [-optfuzz OPTFUZZ]
                      [-name NAME] [-bugs BUGSFOLDER] [-scratch SCRATCHFOLDER] [-opconfig OPCONFIG] [-fusionfun FUSIONFUN] [-km]
                      SOLVER_CLIS PATH_TO_SEEDS [PATH_TO_SEEDS ...]
    yinyang.py: error: the following arguments are required: SOLVER_CLIS, PATH_TO_SEEDS
    

    confuses more than it helps (with all the optional options etc)

    $ python3.9 yinyang.py --help
    usage: yinyang.py [-h] [-s {opfuzz,fusion}] [-o {sat,unsat}] [-i ITERATIONS] [-m MODULO] [-t TIMEOUT] [-d] [-optfuzz OPTFUZZ]
                      [-name NAME] [-bugs BUGSFOLDER] [-scratch SCRATCHFOLDER] [-opconfig OPCONFIG] [-fusionfun FUSIONFUN] [-km]
                      SOLVER_CLIS PATH_TO_SEEDS [PATH_TO_SEEDS ...]
    
    positional arguments:
      SOLVER_CLIS           solvers' command-line interfaces for solving .smt2 files
      PATH_TO_SEEDS         path to the seed files/folders
    
    optional arguments:
      -h, --help            show this help message and exit
      -s {opfuzz,fusion}, --strategy {opfuzz,fusion}
                            set fuzzing strategy
      -o {sat,unsat}, --oracle {sat,unsat}
                            set oracle for semantic fusion strategy (default: unknown)
      -i ITERATIONS, --iterations ITERATIONS
                            set mutating iterations for each seed/pair (default: 300 for Type-Aware Operator Mutation, 30 for
                            SemanticFusion)
      -m MODULO, --modulo MODULO
                            determines when the mutant will be forwarded to the solvers for opfuzz
      -t TIMEOUT, --timeout TIMEOUT
                            set timeout for solving process (default: 8)
      -d, --diagnose        forward solver outputs to stdout e.g. for solver cli diagnosis
      -optfuzz OPTFUZZ, --optfuzz OPTFUZZ
                            read solvers' option setting and enable option fuzzing
      -name NAME, --name NAME
                            set name of this fuzzing instance (default: random string)
      -bugs BUGSFOLDER, --bugsfolder BUGSFOLDER
                            set bug folder (default: /Users/windomin/repositories/yinyang_private/bugs)
      -scratch SCRATCHFOLDER, --scratchfolder SCRATCHFOLDER
                            set scratch folder (default: /Users/windomin/repositories/yinyang_private/scratch)
      -opconfig OPCONFIG, --opconfig OPCONFIG
                            set operator mutation configuration (default:
                            /Users/windomin/repositories/yinyang_private/config/operator_mutations.txt)
      -fusionfun FUSIONFUN, --fusionfun FUSIONFUN
                            set fusion function configuration (default:
                            /Users/windomin/repositories/yinyang_private/config/fusion_functions.txt)
      -km, --keep-mutants   Do not delete the mutants generated in the scratchfolder.
    

    could also be better, with the explanation text more to the right.

    good first issue 
    opened by wintered 1
  • Fixing scoping bug

    Fixing scoping bug

    Issue with quantifiers of the form (forall ((t1 String) (t2 String)) expr in which case t2 would be considered free variable leading to an unsoundness in unsat fusion.

    opened by wintered 0
  • Feat: --keep-seeds command line option

    Feat: --keep-seeds command line option

    Add the command line option --keep-seeds (-k) with default value True. When set to False, scratch files will not be kept in the scratch folder after the Fuzzer executes, but the files will be created anyway.

    opened by nicdard 0
  • [A*] Improve Array type support by moving sort parsing logic from `sort2type` into `AstVisitor`

    [A*] Improve Array type support by moving sort parsing logic from `sort2type` into `AstVisitor`

    I did some major changes on the handling of compound types, e.g. (Array (Array X Y) Y). As far as I understand, in the current code:

    1. The raw parser produces a structured representation of them, e.g. the grammar has all the necessary rules.
    2. The AstVisitor converts this structure into textual representation
    3. The sort2type function converts sort strings back to type objects ( ARRAY_TYPE, BITVECTOR_TYPE, etc.).

    I propose to eliminate sort2type entirely and produce structured type representations in the AstVisitor directly, as done in this PR. This is only halfway done though, as BitVector and FloatingPoint is still parsed in sort2type.

    Apart from that it looks like Opfuzz uses sort2type for constructing rules, so if that is needed then we could move sort2type into the opfuzz module.

    opened by maurobringolf 0
  • [BV] add remaining variants of LT and GT operators

    [BV] add remaining variants of LT and GT operators

    Added support BVUGT, BVUGE, BVSGE, BVSLE. I tested a bit ad-hoc with:

    #!/usr/bin/env bash
    for f in path-to-semantic-fusion-seeds/BV/sat/*.smt2; do
      cp $f tests/unit/test.smt2;
      python -m unittest -k large tests/RunUnitTests.py;
    done
    git checkout tests/unit/test.smt2
    

    and they all pass, same for BV/unsat/. I did not wait for QF_BV to finish, but the first few hundred worked fine.

    opened by maurobringolf 0
  • Parsing error

    Parsing error

    Greetings,

    While trying to parse code written in smtlibv2 through yinyang, I found some bugs that yinyang cannot parse some codes.

    For example, parsing results of yinyang are (None, None) about the below codes.

    Could I know why it happened?

    Thanks for your time!

    (set-info :smt-lib-version 2.6) (set-logic QF_ABV) (set-info :source | Crafted benchmarks created for "Sharing is Caring: Combination of Theories" by Dejan Jovanovic and Clark Barrett. In Proceedings of the 8th International Symposium on Frontiers of Combining Systems (FroCoS '11), Oct. 2011, pp. 195-210. Based on Example 4 from Section 5. |) (set-info :category "crafted") (set-info :status sat) (declare-fun a_0 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_0 () (_ BitVec 128)) (declare-fun a_1 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_1 () (_ BitVec 128)) (declare-fun a_2 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_2 () (_ BitVec 128)) (declare-fun a_3 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_3 () (_ BitVec 128)) (declare-fun a_4 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_4 () (_ BitVec 128)) (declare-fun a_5 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_5 () (_ BitVec 128)) (declare-fun a_6 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_6 () (_ BitVec 128)) (declare-fun a_7 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_7 () (_ BitVec 128)) (declare-fun a_8 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_8 () (_ BitVec 128)) (declare-fun a_9 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_9 () (_ BitVec 128)) (declare-fun a_10 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_10 () (_ BitVec 128)) (declare-fun a_11 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_11 () (_ BitVec 128)) (declare-fun a_12 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_12 () (_ BitVec 128)) (declare-fun a_13 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_13 () (_ BitVec 128)) (declare-fun a_14 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_14 () (_ BitVec 128)) (declare-fun a_15 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_15 () (_ BitVec 128)) (declare-fun a_16 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_16 () (_ BitVec 128)) (declare-fun a_17 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_17 () (_ BitVec 128)) (declare-fun a_18 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_18 () (_ BitVec 128)) (declare-fun a_19 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_19 () (_ BitVec 128)) (declare-fun a_20 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_20 () (_ BitVec 128)) (declare-fun a_21 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_21 () (_ BitVec 128)) (declare-fun a_22 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_22 () (_ BitVec 128)) (declare-fun a_23 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_23 () (_ BitVec 128)) (declare-fun a_24 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_24 () (_ BitVec 128)) (declare-fun a_25 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_25 () (_ BitVec 128)) (declare-fun a_26 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_26 () (_ BitVec 128)) (declare-fun a_27 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_27 () (_ BitVec 128)) (declare-fun a_28 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_28 () (_ BitVec 128)) (declare-fun a_29 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_29 () (_ BitVec 128)) (declare-fun a_30 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_30 () (_ BitVec 128)) (declare-fun a_31 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_31 () (_ BitVec 128)) (declare-fun a_32 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_32 () (_ BitVec 128)) (declare-fun a_33 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_33 () (_ BitVec 128)) (declare-fun a_34 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_34 () (_ BitVec 128)) (declare-fun a_35 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_35 () (_ BitVec 128)) (declare-fun a_36 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_36 () (_ BitVec 128)) (declare-fun a_37 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_37 () (_ BitVec 128)) (declare-fun a_38 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_38 () (_ BitVec 128)) (declare-fun a_39 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_39 () (_ BitVec 128)) (declare-fun a_40 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_40 () (_ BitVec 128)) (declare-fun a_41 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_41 () (_ BitVec 128)) (declare-fun a_42 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_42 () (_ BitVec 128)) (declare-fun a_43 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_43 () (_ BitVec 128)) (declare-fun a_44 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_44 () (_ BitVec 128)) (declare-fun a_45 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_45 () (_ BitVec 128)) (declare-fun a_46 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_46 () (_ BitVec 128)) (declare-fun a_47 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_47 () (_ BitVec 128)) (declare-fun a_48 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_48 () (_ BitVec 128)) (declare-fun a_49 () (Array (_ BitVec 128) (_ BitVec 128))) (declare-fun x_49 () (_ BitVec 128)) (assert (not (= (select a_0 (bvmul x_0 x_1)) (select a_1 (bvmul x_1 x_2))))) (assert (not (= (select a_1 (bvmul x_1 x_2)) (select a_2 (bvmul x_2 x_3))))) (assert (not (= (select a_2 (bvmul x_2 x_3)) (select a_3 (bvmul x_3 x_4))))) (assert (not (= (select a_3 (bvmul x_3 x_4)) (select a_4 (bvmul x_4 x_5))))) (assert (not (= (select a_4 (bvmul x_4 x_5)) (select a_5 (bvmul x_5 x_6))))) (assert (not (= (select a_5 (bvmul x_5 x_6)) (select a_6 (bvmul x_6 x_7))))) (assert (not (= (select a_6 (bvmul x_6 x_7)) (select a_7 (bvmul x_7 x_8))))) (assert (not (= (select a_7 (bvmul x_7 x_8)) (select a_8 (bvmul x_8 x_9))))) (assert (not (= (select a_8 (bvmul x_8 x_9)) (select a_9 (bvmul x_9 x_10))))) (assert (not (= (select a_9 (bvmul x_9 x_10)) (select a_10 (bvmul x_10 x_11))))) (assert (not (= (select a_10 (bvmul x_10 x_11)) (select a_11 (bvmul x_11 x_12))))) (assert (not (= (select a_11 (bvmul x_11 x_12)) (select a_12 (bvmul x_12 x_13))))) (assert (not (= (select a_12 (bvmul x_12 x_13)) (select a_13 (bvmul x_13 x_14))))) (assert (not (= (select a_13 (bvmul x_13 x_14)) (select a_14 (bvmul x_14 x_15))))) (assert (not (= (select a_14 (bvmul x_14 x_15)) (select a_15 (bvmul x_15 x_16))))) (assert (not (= (select a_15 (bvmul x_15 x_16)) (select a_16 (bvmul x_16 x_17))))) (assert (not (= (select a_16 (bvmul x_16 x_17)) (select a_17 (bvmul x_17 x_18))))) (assert (not (= (select a_17 (bvmul x_17 x_18)) (select a_18 (bvmul x_18 x_19))))) (assert (not (= (select a_18 (bvmul x_18 x_19)) (select a_19 (bvmul x_19 x_20))))) (assert (not (= (select a_19 (bvmul x_19 x_20)) (select a_20 (bvmul x_20 x_21))))) (assert (not (= (select a_20 (bvmul x_20 x_21)) (select a_21 (bvmul x_21 x_22))))) (assert (not (= (select a_21 (bvmul x_21 x_22)) (select a_22 (bvmul x_22 x_23))))) (assert (not (= (select a_22 (bvmul x_22 x_23)) (select a_23 (bvmul x_23 x_24))))) (assert (not (= (select a_23 (bvmul x_23 x_24)) (select a_24 (bvmul x_24 x_25))))) (assert (not (= (select a_24 (bvmul x_24 x_25)) (select a_25 (bvmul x_25 x_26))))) (assert (not (= (select a_25 (bvmul x_25 x_26)) (select a_26 (bvmul x_26 x_27))))) (assert (not (= (select a_26 (bvmul x_26 x_27)) (select a_27 (bvmul x_27 x_28))))) (assert (not (= (select a_27 (bvmul x_27 x_28)) (select a_28 (bvmul x_28 x_29))))) (assert (not (= (select a_28 (bvmul x_28 x_29)) (select a_29 (bvmul x_29 x_30))))) (assert (not (= (select a_29 (bvmul x_29 x_30)) (select a_30 (bvmul x_30 x_31))))) (assert (not (= (select a_30 (bvmul x_30 x_31)) (select a_31 (bvmul x_31 x_32))))) (assert (not (= (select a_31 (bvmul x_31 x_32)) (select a_32 (bvmul x_32 x_33))))) (assert (not (= (select a_32 (bvmul x_32 x_33)) (select a_33 (bvmul x_33 x_34))))) (assert (not (= (select a_33 (bvmul x_33 x_34)) (select a_34 (bvmul x_34 x_35))))) (assert (not (= (select a_34 (bvmul x_34 x_35)) (select a_35 (bvmul x_35 x_36))))) (assert (not (= (select a_35 (bvmul x_35 x_36)) (select a_36 (bvmul x_36 x_37))))) (assert (not (= (select a_36 (bvmul x_36 x_37)) (select a_37 (bvmul x_37 x_38))))) (assert (not (= (select a_37 (bvmul x_37 x_38)) (select a_38 (bvmul x_38 x_39))))) (assert (not (= (select a_38 (bvmul x_38 x_39)) (select a_39 (bvmul x_39 x_40))))) (assert (not (= (select a_39 (bvmul x_39 x_40)) (select a_40 (bvmul x_40 x_41))))) (assert (not (= (select a_40 (bvmul x_40 x_41)) (select a_41 (bvmul x_41 x_42))))) (assert (not (= (select a_41 (bvmul x_41 x_42)) (select a_42 (bvmul x_42 x_43))))) (assert (not (= (select a_42 (bvmul x_42 x_43)) (select a_43 (bvmul x_43 x_44))))) (assert (not (= (select a_43 (bvmul x_43 x_44)) (select a_44 (bvmul x_44 x_45))))) (assert (not (= (select a_44 (bvmul x_44 x_45)) (select a_45 (bvmul x_45 x_46))))) (assert (not (= (select a_45 (bvmul x_45 x_46)) (select a_46 (bvmul x_46 x_47))))) (assert (not (= (select a_46 (bvmul x_46 x_47)) (select a_47 (bvmul x_47 x_48))))) (assert (not (= (select a_47 (bvmul x_47 x_48)) (select a_48 (bvmul x_48 x_49))))) (assert (not (= (select a_48 (bvmul x_48 x_49)) (select a_49 (bvmul x_49 x_0))))) (assert (not (= (select a_49 (bvmul x_49 x_0)) (select a_0 (bvmul x_0 x_1))))) (check-sat) (exit)

    opened by fwangdo 1
  • High memory usage

    High memory usage

    yinyang (version 0.3.0 installed via pip) consumes ~40G of memory when running with the provided semantic-fusion-seeds/QF_SLIA seeds. Using more seeds will increase memory consumption (with the QF_SLIA logic from SMT-LIB yinyang runs out of memory on my machine with 128G memory). The memory consumption increases rapidly on startup and seems to be stable after yinyang actually starts fuzzing. The same behavior can be observed with the current git version on master.

    The command I use to run yinyang is: yinyang ./solver.sh semantic-fusion-seeds/QF_SLIA/

    opened by mpreiner 0
  • False typechecker error (expected: Unknown)

    False typechecker error (expected: Unknown)

    This makes the typechecker fail (but z3 and cvc4 are happy with it):

    (declare-fun x () Int)
    (assert (=>
    	(= x 3)
    	(forall ((x Int)) (let ((?y x))
    		(= ?y 3)
    	))
    ))
    (check-sat)
    

    The output is:

    src.parsing.typechecker.TypeCheckError: Ill-typed expression 
    term:           (= x 3)
    faulty subterm: 3
    expected:       Unknown
    actual:         Int
    

    The error disappears when the quantified and global variable have different names.

    bug 
    opened by jiwonparc 0
Releases(v0.3.0)
  • v0.3.0(Aug 18, 2021)

    New features:

    • pip package (#8)
    • TypeFuzz, our most recent Fuzzer (#30)
    • logging (#11)
    • improved usability as a command-line tool
    • code style and code commenting

    Fixes:

    • #19
    • #18
    • #16
    • #15
    • #12
    Source code(tar.gz)
    Source code(zip)
  • v0.2.0(Feb 3, 2021)

    New Features:

    • added documentation
    • new module for fusion strategy to design your own fusion functions
    • quiet mode
    • new logo

    Fixes:

    • several bug fixes in the bug detection logic
    • bugfix src.parsing.Term
    • fixing an unsoundness case in Semantic Fusion
    • malformated .output files
    Source code(tar.gz)
    Source code(zip)
  • v0.1.0(May 7, 2021)

Owner
Project Yin-Yang for SMT Solver Testing
Project Yin-Yang for SMT Solver Testing
An abstraction layer for mathematical optimization solvers.

MathOptInterface Documentation Build Status Social An abstraction layer for mathematical optimization solvers. Replaces MathProgBase. Citing MathOptIn

JuMP-dev 284 Jan 4, 2023
Hydra: an Extensible Fuzzing Framework for Finding Semantic Bugs in File Systems

Hydra: An Extensible Fuzzing Framework for Finding Semantic Bugs in File Systems Paper Finding Semantic Bugs in File Systems with an Extensible Fuzzin

gts3.org (SSLab@Gatech) 129 Dec 15, 2022
PolyGlot, a fuzzing framework for language processors

PolyGlot, a fuzzing framework for language processors Build We tested PolyGlot on Ubuntu 18.04. Get the source code: git clone https://github.com/s3te

Software Systems Security Team at Penn State University 79 Dec 27, 2022
Differential fuzzing for the masses!

NEZHA NEZHA is an efficient and domain-independent differential fuzzer developed at Columbia University. NEZHA exploits the behavioral asymmetries bet

null 147 Dec 5, 2022
InsTrim: Lightweight Instrumentation for Coverage-guided Fuzzing

InsTrim The paper: InsTrim: Lightweight Instrumentation for Coverage-guided Fuzzing Build Prerequisite llvm-8.0-dev clang-8.0 cmake >= 3.2 Make git cl

null 75 Dec 23, 2022
ProFuzzBench - A Benchmark for Stateful Protocol Fuzzing

ProFuzzBench - A Benchmark for Stateful Protocol Fuzzing ProFuzzBench is a benchmark for stateful fuzzing of network protocols. It includes a suite of

null 155 Jan 8, 2023
Emulation and Feedback Fuzzing of Firmware with Memory Sanitization

BaseSAFE This repository contains the BaseSAFE Rust APIs, introduced by "BaseSAFE: Baseband SAnitized Fuzzing through Emulation". The example/ directo

Security in Telecommunications 138 Dec 16, 2022
AntiFuzz: Impeding Fuzzing Audits of Binary Executables

AntiFuzz: Impeding Fuzzing Audits of Binary Executables Get the paper here: https://www.usenix.org/system/files/sec19-guler.pdf Usage: The python scri

Chair for Sys­tems Se­cu­ri­ty 88 Dec 21, 2022
Fuzzification helps developers protect the released, binary-only software from attackers who are capable of applying state-of-the-art fuzzing techniques

About Fuzzification Fuzzification helps developers protect the released, binary-only software from attackers who are capable of applying state-of-the-

gts3.org (SSLab@Gatech) 55 Oct 25, 2022
Fuzzing the Kernel Using Unicornafl and AFL++

Unicorefuzz Fuzzing the Kernel using UnicornAFL and AFL++. For details, skim through the WOOT paper or watch this talk at CCCamp19. Is it any good? ye

Security in Telecommunications 283 Dec 26, 2022
Code for the USENIX 2017 paper: kAFL: Hardware-Assisted Feedback Fuzzing for OS Kernels

kAFL: Hardware-Assisted Feedback Fuzzing for OS Kernels Blazing fast x86-64 VM kernel fuzzing framework with performant VM reloads for Linux, MacOS an

Chair for Sys­tems Se­cu­ri­ty 541 Nov 27, 2022
QSYM: A Practical Concolic Execution Engine Tailored for Hybrid Fuzzing

QSYM: A Practical Concolic Execution Engine Tailored for Hybrid Fuzzing Environment Tested on Ubuntu 14.04 64bit and 16.04 64bit Installation # disabl

gts3.org (SSLab@Gatech) 581 Dec 30, 2022
Fuzzing JavaScript Engines with Aspect-preserving Mutation

DIE Repository for "Fuzzing JavaScript Engines with Aspect-preserving Mutation" (in S&P'20). You can check the paper for technical details. Environmen

gts3.org (SSLab@Gatech) 190 Dec 11, 2022
ParmeSan: Sanitizer-guided Greybox Fuzzing

ParmeSan: Sanitizer-guided Greybox Fuzzing ParmeSan is a sanitizer-guided greybox fuzzer based on Angora. Published Work USENIX Security 2020: ParmeSa

VUSec 158 Dec 31, 2022
Ankou: Guiding Grey-box Fuzzing towards Combinatorial Difference

Ankou Ankou is a source-based grey-box fuzzer. It intends to use a more rich fitness function by going beyond simple branch coverage and considering t

SoftSec Lab 54 Dec 24, 2022
Directed Greybox Fuzzing with AFL

AFLGo: Directed Greybox Fuzzing AFLGo is an extension of American Fuzzy Lop (AFL). Given a set of target locations (e.g., folder/file.c:582), AFLGo ge

null 380 Nov 24, 2022
[ICSE2020] MemLock: Memory Usage Guided Fuzzing

MemLock: Memory Usage Guided Fuzzing This repository provides the tool and the evaluation subjects for the paper "MemLock: Memory Usage Guided Fuzzing

Cheng Wen 54 Jan 7, 2023
A library for performing coverage guided fuzzing of neural networks

TensorFuzz: Coverage Guided Fuzzing for Neural Networks This repository contains a library for performing coverage guided fuzzing of neural networks,

Brain Research 195 Dec 28, 2022
Sound and Cost-effective Fuzzing of Stripped Binaries by Incremental and Stochastic Rewriting

StochFuzz: A New Solution for Binary-only Fuzzing StochFuzz is a (probabilistically) sound and cost-effective fuzzing technique for stripped binaries.

Zhuo Zhang 164 Dec 5, 2022