Merge pull request #41 from testsmt/dev

Dev

.github/workflows/main.yml

@@ -16,9 +16,13 @@ jobs:
  python-version: ${{ matrix.python-version }}
  - name: Install dependencies
  run: |
+ pip install codespell
  python -m pip install flake8
  python -m pip install --upgrade pip 
  python -m pip install antlr4-python3-runtime==4.9.2 
+ - name: Spell check 
+ run: |
+ codespell --skip="Solver.py,SMTLIBv2*,*.g4,*.tokens,*.interp,*.smt2"
  - name: Run Unittests
  run: |
  python -m unittest tests/RunUnitTests.py
@@ -45,3 +49,6 @@ jobs:
  - name: code style and static analysis with flake 
  run: |
  bin/checkstyle.sh
+ - name: pypi check 
+ run: |
+ tests/integration/misc/pypi.sh

.gitignore

@@ -1,2 +1,6 @@
 __pycache__
 .DS_Store
+build
+dist
+logs
+yinyang.egg-info

MANIFEST.in

@@ -0,0 +1 @@
+include yinyang/config/*

README.md

@@ -1,4 +1,4 @@
-<p align="center"><a><img width="130" alt="portfolio_view" align="center" src="media/logo.png"></a></p>
+<p align="center"><a><img width="160" alt="portfolio_view" align="center" src="https://testsmt.github.io/img/tool_logo_with_name.png"></a></p>
 
 <br>
 <p align="center">
@@ -16,20 +16,26 @@
 
 yinyang
 ------------
-A fuzzer 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.
+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
 ------------
-Requirements: 
-- python 3.6+ 
-- antlr4 python runtime 
-``` bash
-git clone https://github.com/testsmt/yinyang.git 
-pip3 install antlr4-python3-runtime==4.9.2 
+To install a stable version of yinyang use: 
+
+```
+pip3 install yinyang
 ```
 
+To install the most recent version, check out the repository: 
+
+``` bash 
+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
 -------------
@@ -40,20 +46,20 @@ to download the corresponding SMT-LIB 2 benchmarks. Alternatively, you can downl
 
 3. **Run yinyang** on the benchmarks e.g. with Z3 and CVC4. 
 ```bash
-bin/opfuzz "z3 model_validate=true;cvc4 --check-models -m -i -q" benchmarks 
+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.
 
-:blue_book: [Documentation](https://yinyang.readthedocs.io/en/latest/)
+📘 [Documentation](https://yinyang.readthedocs.io/en/latest/)
 
 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.
 
- :memo: [Contact us](https://yinyang.readthedocs.io/en/latest/building_on.html#contact)
+📬 [Contact us](https://yinyang.readthedocs.io/en/latest/building_on.html#contact)
 
-Additional Ressources
+Additional Resources
 ----------
 - [Citing yinyang](https://yinyang.readthedocs.io/en/latest/building_on.html#citing-yinyang)
 - [Project website](https://testsmt.github.io/) with bug statistics, talk videos, etc.

bin/checkstyle.sh

@@ -1,2 +1,2 @@
 #! /bin/bash
-flake8 --exclude "*SMTLIBv2*,*runtests.py*,__init__.py" src tests config bin/opfuzz bin/yinyang bin/typefuzz --select=E --ignore=E402 --statistics 
+flake8 --exclude "*SMTLIBv2*,*runtests.py*,__init__.py" yinyang/src tests yinyang/config bin/opfuzz bin/yinyang bin/typefuzz --select=E --ignore=E402 --statistics 

bin/opfuzz

@@ -22,6 +22,7 @@
 # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 # SOFTWARE.
 
+import os
 import sys
 import signal
 import inspect
@@ -31,14 +32,17 @@ path = Path(__file__)
 rootpath = str(path.parent.absolute().parent)
 sys.path.append(rootpath)
 
-from src.base.Driver import run_checks
-from src.base.Error import raise_runtime_error
-from src.base.ArgumentParser import build_opfuzz_parser
-from src.base.Exitcodes import OK_BUGS, OK_NOBUGS, ERR_USAGE, ERR_INTERNAL
+current_dir = os.getcwd()
 
-from src.core.Fuzzer import Fuzzer
+from yinyang.src.base.Driver import run_checks
+from yinyang.src.base.Error import raise_runtime_error
+from yinyang.src.base.ArgumentParser import build_opfuzz_parser
+from yinyang.src.base.Exitcodes import OK_BUGS, OK_NOBUGS
+from yinyang.src.base.Exitcodes import ERR_USAGE, ERR_INTERNAL
 
-from config.OpfuzzHelptext import (
+from yinyang.src.core.Fuzzer import Fuzzer
+
+from yinyang.config.OpfuzzHelptext import (
  usage,
  header,
  short_description,
@@ -48,7 +52,7 @@ from config.OpfuzzHelptext import (
 
 
 def main():
- parser = build_opfuzz_parser(rootpath, usage)
+ parser = build_opfuzz_parser(current_dir, usage)
 
  if len(sys.argv) == 1:
 

bin/typefuzz

@@ -21,7 +21,7 @@
 # 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.
-
+import os
 import sys
 import signal
 import inspect
@@ -31,14 +31,17 @@ path = Path(__file__)
 rootpath = str(path.parent.absolute().parent)
 sys.path.append(rootpath)
 
-from src.base.Driver import run_checks
-from src.base.Error import raise_runtime_error
-from src.base.ArgumentParser import build_typefuzz_parser
-from src.base.Exitcodes import OK_BUGS, OK_NOBUGS, ERR_USAGE, ERR_INTERNAL
+current_dir = os.getcwd()
+
+from yinyang.src.base.Driver import run_checks
+from yinyang.src.base.Error import raise_runtime_error
+from yinyang.src.base.ArgumentParser import build_typefuzz_parser
+from yinyang.src.base.Exitcodes import OK_BUGS, OK_NOBUGS
+from yinyang.src.base.Exitcodes import ERR_USAGE, ERR_INTERNAL
 
-from src.core.Fuzzer import Fuzzer
+from yinyang.src.core.Fuzzer import Fuzzer
 
-from config.TypefuzzHelptext import (
+from yinyang.config.TypefuzzHelptext import (
  usage,
  header,
  short_description,
@@ -48,7 +51,7 @@ from config.TypefuzzHelptext import (
 
 
 def main():
- parser = build_typefuzz_parser(rootpath, usage)
+ parser = build_typefuzz_parser(current_dir, usage)
 
  if len(sys.argv) == 1:
 

bin/yinyang

@@ -22,6 +22,7 @@
 # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 # SOFTWARE.
 
+import os
 import sys
 import signal
 import inspect
@@ -31,14 +32,17 @@ path = Path(__file__)
 rootpath = str(path.parent.absolute().parent)
 sys.path.append(rootpath)
 
-from src.base.Driver import run_checks
-from src.base.Error import raise_runtime_error
-from src.base.ArgumentParser import build_yinyang_parser
-from src.base.Exitcodes import OK_BUGS, OK_NOBUGS, ERR_USAGE, ERR_INTERNAL
+current_dir = os.getcwd()
 
-from src.core.Fuzzer import Fuzzer
+from yinyang.src.base.Driver import run_checks
+from yinyang.src.base.Error import raise_runtime_error
+from yinyang.src.base.ArgumentParser import build_yinyang_parser
+from yinyang.src.base.Exitcodes import OK_BUGS, OK_NOBUGS
+from yinyang.src.base.Exitcodes import ERR_USAGE, ERR_INTERNAL
 
-from config.YinyangHelptext import (
+from yinyang.src.core.Fuzzer import Fuzzer
+
+from yinyang.config.YinyangHelptext import (
  usage,
  header,
  short_description,
@@ -48,7 +52,7 @@ from config.YinyangHelptext import (
 
 
 def main():
- parser = build_yinyang_parser(rootpath, usage)
+ parser = build_yinyang_parser(current_dir, usage)
 
  if len(sys.argv) == 1:
 

docs/basic_usage.rst

@@ -1,13 +1,11 @@
 Basic usage
 ==============
 
-yinyang is a mutation-based fuzzer, i.e. it mutates a set of seed formulas using a mutation strategy and then uses the mutated formulas as the test seeds for SMT solvers. yinyang can so detect soundness bugs, invalid model bugs, crashes, segfaults, etc. Its default mutation strategy is ``opfuzz`` which generates mutants by interchanging operators, e.g, ``=,distinct,+,-, *,/``. 
-
-You can run yinyang with the ``opfuzz`` strategy using the following command: 
+yinyang is a mutation-based fuzzer, i.e. it mutates a set of seed formulas using a mutation strategy and then uses the mutated formulas as the test seeds for SMT solvers. yinyang can so detect soundness bugs, invalid model bugs, crashes, segfaults, etc. With ``typefuzz`` we generate mutants by generating fresh expressions from the ones from the seed and root them by operators such as ``=,distinct,+,-, *,/`` by one another. You can run yinyang with the ``typefuzz`` strategy using the following command: 
 
 .. code-block:: bash
  
- $ python3 yinyang.py "<solver_clis>" <seed_path>
+ $ typefuzz "<solver_clis>" <seed_path>
 
 - ``<solver_clis>``: a sequence of SMT solvers command lines separated by semicolons. At least two SMT solvers command lines are necessary. 
 
@@ -19,7 +17,7 @@ You can run yinyang with the ``opfuzz`` strategy using the following command:
 
 .. code-block:: bash
  
- $ python3 yinyang.py "z3 model_validate=true;cvc4 --check-models -m -i -q" benchmarks 
+ $ typefuzz "z3 model_validate=true;cvc4 --check-models -m -i -q" benchmarks 
 
 
 yinyang will by default randomly select formulas from the folder ``./benchmarks``. By default SMT-LIB files larger than 20k will be ignored. yinyang will generate 300 mutants per seed formula and will run in an infinite loop. You can use the shortcut ``CTRL+C`` to terminate yinyang manually. If a bug has been found, the bug trigger is stored in ``./bugs``.
@@ -28,4 +26,4 @@ yinyang will by default randomly select formulas from the folder ``./benchmarks`
  To catch invalid model bugs, you have to supply options to enable model validation in ``<solver_clis>``. Also consider that you may need to supply options to enable model production and incremental mode to command lines in ``<solver_clis>``.
 
 **Reducing a bug**.
-After finding a bug, it is useful to produce a minimal test case before reporting the bug to save the SMT solver developers' time and effort. For many test cases, the C code reducer `creduce <https://embed.cs.utah.edu/creduce/>`_ does a great job. Besides, SMT-LIB specific reducer `pyDelta <https://github.com/nafur/pydelta>`_ can be used. 
+After finding a bug, it is useful to produce a minimal test case before reporting the bug to save the SMT solver developers' time and effort. For many test cases, the C code reducer `creduce <https://embed.cs.utah.edu/creduce/>`_ does a great job. Besides, SMT-LIB specific reducer `pydelta <https://github.com/nafur/pydelta>`_ can be used.