Merge pull request #40 from testsmt/pypi

Pypi
testsmt · Aug 18, 2021 · e2fcec5 · e2fcec5
2 parents 18e4aae + b81f678
commit e2fcec5
Show file tree

Hide file tree

Showing 74 changed files with 152 additions and 136 deletions.
diff --git a/.gitignore b/.gitignore
@@ -2,4 +2,5 @@ __pycache__
 .DS_Store
 build
 dist
+logs
 yinyang.egg-info
diff --git a/MANIFEST.in b/MANIFEST.in
@@ -0,0 +1 @@
+include yinyang/config/*
diff --git a/bin/checkstyle.sh b/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 
diff --git a/bin/opfuzz b/bin/opfuzz
@@ -34,14 +34,15 @@ sys.path.append(rootpath)
 
 current_dir = os.getcwd()
 
-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
+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 src.core.Fuzzer import Fuzzer
+from yinyang.src.core.Fuzzer import Fuzzer
 
-from config.OpfuzzHelptext import (
+from yinyang.config.OpfuzzHelptext import (
  usage,
  header,
  short_description,
@@ -51,7 +52,7 @@ from config.OpfuzzHelptext import (
 
 
 def main():
- parser = build_opfuzz_parser(rootpath, current_dir, usage)
+ parser = build_opfuzz_parser(current_dir, usage)
 
  if len(sys.argv) == 1:
 

diff --git a/bin/typefuzz b/bin/typefuzz
@@ -33,14 +33,15 @@ sys.path.append(rootpath)
 
 current_dir = os.getcwd()
 
-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
+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,
@@ -50,7 +51,7 @@ from config.TypefuzzHelptext import (
 
 
 def main():
- parser = build_typefuzz_parser(rootpath, current_dir, usage)
+ parser = build_typefuzz_parser(current_dir, usage)
 
  if len(sys.argv) == 1:
 

diff --git a/bin/yinyang b/bin/yinyang
@@ -34,14 +34,15 @@ sys.path.append(rootpath)
 
 current_dir = os.getcwd()
 
-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
+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 src.core.Fuzzer import Fuzzer
+from yinyang.src.core.Fuzzer import Fuzzer
 
-from config.YinyangHelptext import (
+from yinyang.config.YinyangHelptext import (
  usage,
  header,
  short_description,
@@ -51,7 +52,7 @@ from config.YinyangHelptext import (
 
 
 def main():
- parser = build_yinyang_parser(rootpath, current_dir, usage)
+ parser = build_yinyang_parser(current_dir, usage)
 
  if len(sys.argv) == 1:
 

diff --git a/docs/building_on.rst b/docs/building_on.rst
@@ -30,7 +30,7 @@ The following file tree shows the most important files of typefuzz and includes
 
 When TypeFuzz is called from the command line, it executes `bin/typefuzz` containing the main function. After parsing the command line and reading in the seeds, the method `Fuzzer.py:run` is called. It randomly pops an SMT-LIB file from the seed list (`Fuzzer.py:142`), then parses (`Fuzzer.py:98`) and type-checks (`Fuzzer.py:146`) the SMT-LIB file. Next, we compute the set of unique expressions (`Fuzzer.py:148`) from the seed and pass it to a newly created mutator GenTypeAwareMutation (`Fuzzer.py:149`). The mutator is then called in a for-loop realizing n consecutive mutations (`Fuzzer.py:171`). Each mutated formula is then passed to the SMT solvers under test which checks for soundness bugs, invalid model bugs, assertion violations, segfaults (`Fuzzer.py:185`) and dumps the bug triggers to the disk. For details on these checks, read the comments in the method `Fuzzer.py:test`. 
 
-Generative type-aware mutation's mutator class is realized in `GenTypeAwareMutation.py`. It takes a type-checked SMT-LIB script and the set of its unique expressions as arguments to the constructor. Then, we parse the configuration file (`config/typefuzz_config.txt`) containing the operator signatures. The method `mutate` implements a mutation step. First, we call the method `get_all_subterms` to return a list of all expressions (`av_expr`) and another list with their types (`expr_type`). Next, we repeatedly choose a term t1 from the formula to be substituted by a term t2 (returned by `get_replacee`). If we could successfully construct such a term, then we substitute and return the mutated formula.
+Generative type-aware mutation's mutator class is realized in `GenTypeAwareMutation.py`. It takes a type-checked SMT-LIB script and the set of its unique expressions as arguments to the constructor. Then, we parse the configuration file (`yinyang/config/typefuzz_config.txt`) containing the operator signatures. The method `mutate` implements a mutation step. First, we call the method `get_all_subterms` to return a list of all expressions (`av_expr`) and another list with their types (`expr_type`). Next, we repeatedly choose a term t1 from the formula to be substituted by a term t2 (returned by `get_replacee`). If we could successfully construct such a term, then we substitute and return the mutated formula.
 
 The `get_replacee(term)` method randomly chooses an operator from the list of candidate operators. The list of candidate operators contains all operators with a return type matching term's type and includes the identity operator `id`. Next, we pick a type-conforming expression from the set of unique expressions for every argument for the operator at hand and return the expression. The `get_replacee`method may fail, e.g., if we would have picked an operator of a conforming type but no term with conforming types to its arguments exist. To avoid this, we repeat the `get_replacee` method several times.
 
@@ -42,7 +42,7 @@ Run TypeFuzz with other SMT Solvers
 ....................................
 Besides Z3 and CVC4, TypeFuzz can be run with any other SMT solver such as [MathSAT](http://mathsat.fbk.eu), [Boolector](http://verify.inf.usi.ch/content/opensmt2), [Yices](http://yices.csl.sri.com/), and [SMT-Interpol](http://ultimate.informatik.uni-freiburg.de/smtinterpol/), etc. Since TypeFuzz is based on differential testing, it needs at least two solver configurations, ideally with a large overlap in the supported SMT logics. Furthermore, yinyang's type checker currently has stable support for string and arithmetic logics. Support for other logics is currently experimental but will be finalized shortly.
 
-Solver configurations could either be specified in the command line or in the configuration file `config/Config.py` such as: 
+Solver configurations could either be specified in the command line or in the configuration file `yinyang/config/Config.py` such as: 
 .. code-block:: text
 
  solvers = [
@@ -52,7 +52,7 @@ Solver configurations could either be specified in the command line or in the co
  "cvc4 --check-models --produce-models --incremental --strings-exp -q",
  ]
 
-To run TypeFuzz with these four solver configurations in the config file, you would need to run `typefuzz "" <benchmark-dir>`. Note, the `crash_list` in Config/config.py, which may need to be updated ensuring that crashes by the new solver(s) are caught.
+To run TypeFuzz with these four solver configurations in the config file, you would need to run `typefuzz "" <benchmark-dir>`. Note, the `crash_list` in yinyang/config/config.py, which may need to be updated ensuring that crashes by the new solver(s) are caught.
 
 Devise a custom mutator 
 .........................

diff --git a/docs/fusion.rst b/docs/fusion.rst
@@ -54,7 +54,7 @@ Fusion requires the seeds that are pre-categorized to be either sat or unsat. Pr
 
 Fusion functions
 ................................
-The configuration file ``config/fusion_functions.txt`` specifies fusion and inversion functions. The format is the following: 
+The configuration file ``yinyang/config/fusion_functions.txt`` specifies fusion and inversion functions. The format is the following: 
 
 .. code-block:: text 
 
@@ -70,7 +70,7 @@ The configuration file ``config/fusion_functions.txt`` specifies fusion and inve
 
 **Example:**
 
-The following code shows schematically fusion and inversion are described in ``config/fusion_functions.txt``.
+The following code shows schematically fusion and inversion are described in ``yinyang/config/fusion_functions.txt``.
 
 .. code-block:: text 
 

diff --git a/setup.cfg b/setup.cfg
@@ -1,6 +1,6 @@
 [metadata]
 name = yinyang
-version = 0.1.0
+version = 0.3.0
 author = Dominik Winterer, Chengyu Zhang, Jiwon Park, Zhendong Su
 author_email = [email protected], [email protected], [email protected], ‎[email protected]
 description = A fuzzing framework for SMT solvers
@@ -17,6 +17,7 @@ classifiers =
  Operating System :: OS Independent
 
 [options]
+include_package_data = True
 packages = find:
 install_requires =
  antlr4-python3-runtime==4.9.2

diff --git a/tests/integration/detection/TestDetection.py b/tests/integration/detection/TestDetection.py
@@ -349,8 +349,8 @@ def test_duplicate_list():
 ]
 
 """
- os.system("mv config/config.py config/config.py.orig")
- with open("config/Config.py", "w") as f:
+ os.system("mv yinyang/config/config.py yinyang/config/config.py.orig")
+ with open("yinyang/config/Config.py", "w") as f:
  f.write(config_py)
  create_mocksolver_msg(msg, solver)
  first_config = os.path.abspath(solver)
@@ -364,7 +364,7 @@ def test_duplicate_list():
  exit(1)
  else:
  os.system("rm -rf " + solver)
- os.system("mv config/config.py.orig config/config.py")
+ os.system("mv yinyang/config/config.py.orig yinyang/config/config.py")
 
 
 if __name__ == "__main__":

diff --git a/tests/integration/parsing/ast/Ast.py b/tests/integration/parsing/ast/Ast.py
@@ -24,10 +24,10 @@
 
 from antlr4.CommonTokenStream import FileStream, CommonTokenStream
 
-from src.parsing.SMTLIBv2Lexer import SMTLIBv2Lexer
-from src.parsing.SMTLIBv2Parser import SMTLIBv2Parser
-from src.parsing.AstVisitor import AstVisitor
-from src.parsing.Parse import parse_file
+from yinyang.src.parsing.SMTLIBv2Lexer import SMTLIBv2Lexer
+from yinyang.src.parsing.SMTLIBv2Parser import SMTLIBv2Parser
+from yinyang.src.parsing.AstVisitor import AstVisitor
+from yinyang.src.parsing.Parse import parse_file
 
 sys.setrecursionlimit(100000)
 sys.path.append("../../../../")

diff --git a/tests/integration/parsing/ast/CheckOutput.py b/tests/integration/parsing/ast/CheckOutput.py
@@ -30,9 +30,9 @@
 
 from antlr4.CommonTokenStream import FileStream, CommonTokenStream
 
-from src.parsing.SMTLIBv2Lexer import SMTLIBv2Lexer
-from src.parsing.SMTLIBv2Parser import SMTLIBv2Parser
-from src.parsing.AstVisitor import AstVisitor
+from yinyang.src.parsing.SMTLIBv2Lexer import SMTLIBv2Lexer
+from yinyang.src.parsing.SMTLIBv2Parser import SMTLIBv2Parser
+from yinyang.src.parsing.AstVisitor import AstVisitor
 
 
 sys.setrecursionlimit(100000)

diff --git a/tests/integration/parsing/parser/Parse.py b/tests/integration/parsing/parser/Parse.py
@@ -23,8 +23,8 @@
 import sys
 
 from antlr4.CommonTokenStream import CommonTokenStream, FileStream
-from src.parsing.SMTLIBv2Lexer import SMTLIBv2Lexer
-from src.parsing.SMTLIBv2Parser import SMTLIBv2Parser
+from yinyang.src.parsing.SMTLIBv2Lexer import SMTLIBv2Lexer
+from yinyang.src.parsing.SMTLIBv2Parser import SMTLIBv2Parser
 
 sys.setrecursionlimit(100000)
 sys.path.append("../../")

diff --git a/tests/unit/TestGenTypeAwareMutation.py b/tests/unit/TestGenTypeAwareMutation.py
@@ -26,15 +26,15 @@
 sys.path.append("../../")
 import os
 
-from src.parsing.Parse import *
-from src.parsing.Typechecker import Context, typecheck
-from src.mutators.GenTypeAwareMutation.GenTypeAwareMutation import *
-from src.mutators.GenTypeAwareMutation.Util import *
+from yinyang.src.parsing.Parse import *
+from yinyang.src.parsing.Typechecker import Context, typecheck
+from yinyang.src.mutators.GenTypeAwareMutation.GenTypeAwareMutation import *
+from yinyang.src.mutators.GenTypeAwareMutation.Util import *
 
 
 class Mockargs:
  modulo = 3
- config = "config/typefuzz_config.txt"
+ config = "yinyang/config/typefuzz_config.txt"
 
 
 class GenTypeAwareMutationTestCase(unittest.TestCase):

diff --git a/tests/unit/TestLocalVariables.py b/tests/unit/TestLocalVariables.py
@@ -26,16 +26,16 @@
 
 sys.path.append("../../")
 
-from src.parsing.parse import *
-from src.parsing.typechecker import Context, typecheck
-from src.generators.TypeAwareOpMutation import TypeAwareOpMutation
-from src.generators.GenTypeAwareMutation.GenTypeAwareMutation import *
-from src.generators.GenTypeAwareMutation.Util import *
+from yinyang.src.parsing.parse import *
+from yinyang.src.parsing.typechecker import Context, typecheck
+from yinyang.src.generators.TypeAwareOpMutation import TypeAwareOpMutation
+from yinyang.src.generators.GenTypeAwareMutation.GenTypeAwareMutation import *
+from yinyang.src.generators.GenTypeAwareMutation.Util import *
 
 
 class Mockargs:
  modulo = 3
- config_file = "config/generalization.txt"
+ config_file = "yinyang/config/generalization.txt"
 
 
 class LocalVariableMutationTestCase(unittest.TestCase):

diff --git a/tests/unit/TestParsing.py b/tests/unit/TestParsing.py
@@ -23,7 +23,7 @@
 import unittest
 import sys
 
-from src.parsing.Parse import parse_str, parse_file
+from yinyang.src.parsing.Parse import parse_str, parse_file
 
 sys.path.append("../../")
 

diff --git a/tests/unit/TestSemanticFusion.py b/tests/unit/TestSemanticFusion.py
@@ -23,8 +23,8 @@
 import sys
 import unittest
 
-from src.parsing.Parse import parse_file
-from src.mutators.SemanticFusion.SemanticFusion import SemanticFusion
+from yinyang.src.parsing.Parse import parse_file
+from yinyang.src.mutators.SemanticFusion.SemanticFusion import SemanticFusion
 
 sys.path.append("../../")
 

diff --git a/tests/unit/TestTerm.py b/tests/unit/TestTerm.py
@@ -23,8 +23,8 @@
 import sys
 import unittest
 
-from src.parsing.Parse import parse_str
-from src.parsing.Ast import Const, Var, Expr
+from yinyang.src.parsing.Parse import parse_str
+from yinyang.src.parsing.Ast import Const, Var, Expr
 
 sys.path.append("../../")
 

diff --git a/tests/unit/TestTypeAwareOpMutation.py b/tests/unit/TestTypeAwareOpMutation.py
@@ -23,8 +23,8 @@
 import sys
 import unittest
 
-from src.parsing.Parse import parse_str, parse_file
-from src.mutators.TypeAwareOpMutation import TypeAwareOpMutation
+from yinyang.src.parsing.Parse import parse_str, parse_file
+from yinyang.src.mutators.TypeAwareOpMutation import TypeAwareOpMutation
 
 sys.path.append("../../")
 

diff --git a/tests/unit/TestTypechecker.py b/tests/unit/TestTypechecker.py
@@ -26,21 +26,21 @@
 
 sys.path.append("../../")
 
-from src.parsing.Ast import (
+from yinyang.src.parsing.Ast import (
  Assert,
 )
-from src.parsing.Parse import (
+from yinyang.src.parsing.Parse import (
  parse_str, parse_file
 )
 
-from src.parsing.Types import (
+from yinyang.src.parsing.Types import (
  UNKNOWN,
  BOOLEAN_TYPE,
  INTEGER_TYPE,
  STRING_TYPE,
 )
 
-from src.parsing.Typechecker import Context, typecheck_expr, typecheck
+from yinyang.src.parsing.Typechecker import Context, typecheck_expr, typecheck
 
 
 def check_type(expr):

diff --git a/config/__init__.py → yinyang/__init__.py b/config/__init__.py → yinyang/__init__.py
diff --git a/config/Config.py → yinyang/config/Config.py b/config/Config.py → yinyang/config/Config.py
diff --git a/config/OpfuzzHelptext.py → yinyang/config/OpfuzzHelptext.py b/config/OpfuzzHelptext.py → yinyang/config/OpfuzzHelptext.py
@@ -20,7 +20,7 @@
 # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 # SOFTWARE.
 
-from src.base.Version import VERSION
+from yinyang.src.base.Version import VERSION
 
 
 header = (

diff --git a/config/TypefuzzHelptext.py → yinyang/config/TypefuzzHelptext.py b/config/TypefuzzHelptext.py → yinyang/config/TypefuzzHelptext.py
@@ -20,7 +20,7 @@
 # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 # SOFTWARE.
 
-from src.base.Version import VERSION
+from yinyang.src.base.Version import VERSION
 
 
 header = (
@@ -119,7 +119,8 @@
  -s <path>, --scratchfolder <path>
  temp folder to dump mutants (default: ./scratch)
  -c <file>, --config <file>
- set custom config file. (default: config/typefuzz_config.txt)
+ set custom config file. 
+ (default: yinyang/config/typefuzz_config.txt)
  -L <bytes>, --limit <bytes>
  file size limit on seed formula in bytes (default: 100000)
  -n, --no-log disable logging

diff --git a/config/YinyangHelptext.py → yinyang/config/YinyangHelptext.py b/config/YinyangHelptext.py → yinyang/config/YinyangHelptext.py
@@ -20,7 +20,7 @@
 # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 # SOFTWARE.
 
-from src.base.Version import VERSION
+from yinyang.src.base.Version import VERSION
 
 
 header = (

diff --git a/src/__init__.py → yinyang/config/__init__.py b/src/__init__.py → yinyang/config/__init__.py
diff --git a/config/fusion_functions.txt → yinyang/config/fusion_functions.txt b/config/fusion_functions.txt → yinyang/config/fusion_functions.txt
diff --git a/config/operator_mutations.txt → yinyang/config/operator_mutations.txt b/config/operator_mutations.txt → yinyang/config/operator_mutations.txt
diff --git a/config/option_setting.txt → yinyang/config/option_setting.txt b/config/option_setting.txt → yinyang/config/option_setting.txt
diff --git a/config/typefuzz_config.txt → yinyang/config/typefuzz_config.txt b/config/typefuzz_config.txt → yinyang/config/typefuzz_config.txt
diff --git a/src/base/__init__.py → yinyang/src/__init__.py b/src/base/__init__.py → yinyang/src/__init__.py