testsmt / yinyang Goto Github PK

View Code? Open in Web Editor NEW

177.0 6.0 22.0 3.1 MB

A fuzzing framework for SMT solvers

Home Page: https://testsmt.github.io/

License: MIT License

Python 53.37% ANTLR 1.23% Shell 0.49% SMT 44.91%

testing smt-solver z3 cvc4 smt-lib smt fuzzing

yinyang's Introduction

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 ffg

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

Usage

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.
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.
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

Citing yinyang
Project website with bug statistics, talk videos, etc.
Google Open Source Peer Bonus 🏆
Amazon Research Awards 🏆

yinyang's People

Contributors

Stargazers

Watchers

yinyang's Issues

Extend to support all logics (Typechecker)

This mostly means to make the type-checker capable of dealing with SMT-LIB files of all logics. It is already implemented but not yet robust enough.

Parser rejects variables with prefix "bv"

Commit: d8174eb

The parser currently rejects formulas such as the one below.

(declare-fun bv () (_ BitVec 10))                                               
(declare-fun a () Bool)                                                         
(assert (not (and (= ((_ extract 5 3) (_ bv96 8)) ((_ extract 4 2) (concat (_ bv121 7) 
((_ extract 0 0) bv)))) (= (concat (_ bv1 1) (ite a (_ bv0 1) (_ bv1 1))) ((_ extract 1 0) 
(ite a (_ bv6 3) (_ bv3 3)))))))
(check-sat)

Reason being the declared variable "bv" which seems to conflict with rules for bitvector constants such as "(_ bv0 1)". When there are no variables with prefix "bv", then parsing succeeds.

Automate regression tests for fusion

Integrate Typefuzz

Exception while running typefuzz on the remote server

Bug Description

While trying to use typefuzz on Ubuntu Linux

Linux mantella 5.4.0-159-generic #176-Ubuntu SMP Mon Aug 14 12:04:20 UTC 2023 x86_64 x86_64 x86_64 GNU/Linux

It returns an error, trying to iterate on argument of type "Term"

Note

Possibly it is due to the command, as cvc5 is not installed on the machine, and I try to provide it by giving the executable path in the command:

./bin/typefuzz "z3 model_validate=true;../cvc5/build/bin/cvc5 --check-models -m -i -q" ../opensmt/regression/QF_UF/NEQ004_size4.smt│2

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

Add script for running yinyang in parallel mode

Actions:

devise parallel run script
make sure some logs are generated so errors can be diagnosed quickly; add it to scripts
provide 1-2 sentence documentation on how to run it

Using empty fusion_function file makes yinyang hang.

Performance fuzzing

Is there any existing code for performance fuzzing or would that be a new feature?

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

Print warning when no solvers specified

Refactoring and code style

Actions:

refactoring
code reviews
integrate code style checker, e.g. based on PEP into travis to be checked at each commit

Support for Z3 tactics

Add support the testing of z3 tactics (and also the ability to test both options and tactics.

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/

logging

Deepcopy interrupt the execution.

When taking QF_NRA benchmarks atan-vega-3-chunk-0596.smt2 and ball_count_2d_hill_simple.04.seq_lazy_global_13.smt2 as the fusion seeds, yinyang will unexpectedly terminate without giving any information. The root cause seems to be that deepcopy terminates the execution at the following line:

yinyang/yinyang/src/mutators/SemanticFusion/SemanticFusion.py

Line 145 in f38bb10

copy.deepcopy(self.formula1), copy.deepcopy(self.formula2)

We need to investigate further to see whether it is a bug in deepcopy and how to address it.

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)

More general option fuzzing

Make option fuzzing for cvc4 to be more general (not only boolean flags) and abide by their fuzzing guidelines

pip package

Prepare a pip package to allow users to install stable versions of yinyang.

Actions

work through https://packaging.python.org/tutorials/packaging-projects/
clarify how to allow users to customize the fuzzer if they do not have the code in the working directory?

Cannot detect soundness issue when (get-model) is in the mutant.

When there is a (get-mode) in the seeds, the mutant will also bring a (get-model) after mutation.
If we use this mutant to test SMT solvers, the solvers would report:

unsat
(error "line 13 column 10: model is not available")

sat
(error "Cannot get model when produce-models options is off.")

Since they contain error, such outputs will be ignored by yinyang even though this mutant triggers a soundness bug.
We could get rid of (get-model) in our mutants.

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

Parser bug on formula with string escape sequences

from src.parsing.parse import *                                                    
formula_str=\                                                                      
"""                                                                                
(define-const a String "\x0a")                                                     
(define-const c String "\n")                                                       
(simplify (= a b))                                                                 
(simplify (str.++ a b))"""                                                         
formula,_ = parse_str(formula_str)                                                 
print(formula)                                                                     
# Output:                                                                          
# (define-const a String "                                                         
# ")                                                                               
# (define-const c String "                                                         
# ")                                                                               
# (simplify (= a b))                                                               
# (simplify (str.++ a b))

Commit: 58e8aed

Issue with regex constants re.allchar

Some regex constants, i.e., re.none, re.all, and re.allchar, from the config/generalization.txt need some special treatment as they are constants. At the moment, when they are used, extra '(' and ')' are added, e.g., (re.none), which leads to errors.

Typed expressions

Extend DSL of OpFuzz config file

+,-,*,/  :type Real
+,-,*, div, mod :type Int

Action:

Extend DSL parser to accept type as an argument

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.

Sanity check for type-checking on the currently supported logics

Infrequent application of id rule

The rule for "(par (A) (id A A))" might be enabled too infrequently as there are many other rules in the config rule. Not sure what would be the best way to deal with it, and how often it should be triggered; perhaps throw a random coin when we perform a mutation, say with probability p=0.1, we use it, otherwise, the other rules will be used. If p=1.0, it should be the same as what we have already.

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.

Increase robustness of Typefuzz

make Typefuzz more robust as it fails on several benchmarks
Related issues: #31 , #33, #34

testsmt / yinyang Goto Github PK

yinyang's Introduction

yinyang

Installation

Usage

Feedback

Additional Resources

yinyang's People

Contributors

Stargazers

Watchers

Forkers

yinyang's Issues

Bug Description

Note

Recommend Projects

Recommend Topics

Recommend Org