Skip to content

Commit

Permalink
Merge pull request #78 from nicdard/feat/package
Browse files Browse the repository at this point in the history
fix: change old src path to ffg
  • Loading branch information
nicdard authored Sep 16, 2022
2 parents 7d4dbed + 77c0d16 commit 5ff3846
Show file tree
Hide file tree
Showing 8 changed files with 87 additions and 17 deletions.
4 changes: 2 additions & 2 deletions .dockerignore
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
# Ignore everything
*
# Include src
!/src
# Include ffg
!/ffg
!/scripts
!main.py
!README.md
Expand Down
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ We use wheel, just run:
> python3 setup.py bdist_wheel
Use the following command to install the package locally (add `-e` to enable hot reloading):
> python3 -m pip3 install .
> python3 -m pip install .
## Setup and using yinyang

Expand Down
2 changes: 1 addition & 1 deletion benchmarking/coverage.sh
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ help()

if [ ! -z $1 ]; then
echo "Compute coverage information for $1"
gcovr --json-summary-pretty --json-summary --root /app/$1/src --object-directory /app/$1/build/ -o $2/coverage.json
gcovr --json-summary-pretty --json-summary --root /app/$1/ffg --object-directory /app/$1/build/ -o $2/coverage.json
echo "The coverage report can be found here: $2/coverage.json"
else
help
Expand Down
51 changes: 51 additions & 0 deletions ffg/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,51 @@
# fusion-function-generator (ffg)

![CI](https://github.com/nicdard/fusion-function-generator/actions/workflows/ci.yml/badge.svg)

Automatic generation of [Fusion Functions](https://yinyang.readthedocs.io/en/latest/fusion.html#fusion-functions)
used by
[yinyang](https://yinyang.readthedocs.io/en/latest/index.html) fuzzer for [Semantic Fusion](https://yinyang.readthedocs.io/en/latest/fusion.html).

## Lib structure

The package is divided into 4 folders:
* gen
* operators
* visitors
* emitter

The folder `gen` contains the code which is used to generate the whole
`operators` folder, the [configuration file](ffg/gen/gen_configuration.py) exposing some api to control which operators to use during the generation of the tree as well as some constants for the options to the generation algorithm.
the file `tree_generation` instead contains the main tree generation algorithm.

`operators` contains the basic definition of the operators classes.

`visitors` folder contains useful api to print, export to DOT format and rewrite the trees to their inverses.

Finally, `emitter` includes the code needed to export fusion functions to the format understood by YinYang. It also contains an emitter that outputs fusion functions and its inverses to DOT file.

## Cookbook

Use only a subset of the theories in the generation:
```python
ffg.gen.gen_configuration.set_available_theories(['bool', 'real'])
```

Get the available theories:
```python
ffg.gen.gen_configuration.get_theories()
```

Generate a fusion function of two vairables (as a tree):
```python
tree, _ = ffg.gen.tree_generation.generate_tree(root_type, size, ['x', 'y'], 'z')
```

Emit the fusion function to YinYang format as a string:
```python
output = io.StringIO()
emit_function(tree, output, is_wrapped=False)
ff = output.getvalue()
```


14 changes: 8 additions & 6 deletions ffg/emitter/yinyang_emitter.py
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,7 @@ def emit_options(file, args):
print("", file=file)


def emit_function(tree: Operator, file):
def emit_function(tree: Operator, file, wrap=True):
"""
Emits a fusion function and its inverses to yinyang's configuration file:
#begin
Expand All @@ -67,16 +67,17 @@ def emit_function(tree: Operator, file):
For more information on the format please visit:
https://yinyang.readthedocs.io/en/latest/fusion.html#fusion-functions
is_symbolic: when traversing constants, emits either the names (true) or the values (false).
is_wrapped: emit also #begin and #end lines.
"""

rewriter = RewriteVisitor()
printer = PrinterVisitor()
variables = tree.accept(VariableVisitor())
constants = tree.accept(ConstantVisitor())

# Block begin
print("#begin", file=file)
if wrap:
# Block begin
print("#begin", file=file)

# Variable declarations
for variable, type in sorted(variables.items()):
Expand All @@ -93,5 +94,6 @@ def emit_function(tree: Operator, file):
for inverse_root in tree.accept(rewriter):
print(f"(assert {inverse_root.accept(printer)})", file=file)

# Block end
print("#end\n", file=file)
if wrap:
# Block end
print("#end\n", file=file)
23 changes: 17 additions & 6 deletions ffg/gen/gen_configuration.py
Original file line number Diff line number Diff line change
Expand Up @@ -124,15 +124,26 @@
"BitVectorOperator": "BitVectorEquality",
}

BOOLEAN_OPTION = "bool"
INT_OPTION = "int"
REAL_OPTION = "real"
STRING_OPTION = "string"
BITVECTOR_OPTION = "bitvector"


# A map from command line options to the internal representation.
_option_to_operator_type: Dict[str, str] = {
"bool": "BooleanOperator",
"int": "IntegerOperator",
"real": "RealOperator",
"string": "StringOperator",
"bitvector": "BitVectorOperator",
BOOLEAN_OPTION: "BooleanOperator",
INT_OPTION: "IntegerOperator",
REAL_OPTION: "RealOperator",
STRING_OPTION: "StringOperator",
BITVECTOR_OPTION: "BitVectorOperator",
}


THEORY_OPTIONS = list(_option_to_operator_type.keys())


_available_theories: List[str] = list(theory_declarations.keys())


Expand Down Expand Up @@ -215,5 +226,5 @@ def get_module_name(theory: str) -> str:

def get_operator_class(theory: str, name: str) -> 'Operator.__class__':
module_name = get_module_name(theory)
module = importlib.import_module('src.operators.' + module_name)
module = importlib.import_module('ffg.operators.' + module_name)
return getattr(module, name)
2 changes: 1 addition & 1 deletion main.py
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ def parse_args():
default='fusion_functions', help='name of the output file')
parser.add_argument('--dot', '-d', action='store_true',
help='emit formulas and inverses also to dot files')
parser.add_argument('--theories', choices=['bool', 'int', 'real', 'string', 'bitvector'], nargs='+',
parser.add_argument('--theories', choices=gen_configuration.THEORY_OPTIONS, nargs='+',
default=[], help='specify the theories to be used during generation')
return parser.parse_args()

Expand Down
6 changes: 6 additions & 0 deletions setup.py
Original file line number Diff line number Diff line change
Expand Up @@ -20,13 +20,19 @@
# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
# SOFTWARE.

from pathlib import Path
from setuptools import find_packages, setup

this_directory = Path(__file__).parent
long_description = (this_directory / "ffg/README.md").read_text()

setup(
name='ffg',
packages=find_packages(exclude=['tests']),
version='0.1.0',
description='A generator of fusion functions for Semantic Fusion (YinYang).',
author='Nicola Dardanis, Lucas Weitzendorf',
license='MIT',
long_description=long_description,
long_description_content_type='text/markdown',
)

0 comments on commit 5ff3846

Please sign in to comment.