Skip to content

feat bundle: concolic generation, adapting latest TF, and more #66

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
ganler merged 1 commit into from
Dec 30, 2022
Merged

feat bundle: concolic generation, adapting latest TF, and more #66

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 11 additions & 4 deletions .github/workflows/ci.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,12 +25,19 @@ jobs:
- name: Test TensorFlow
run: |
pytest tests/tensorflow
- name: Test CLI [model_gen + model_exec]
- name: Test CLI [Symbolic model_gen + model_exec]
run: |
yes | python nnsmith/cli/model_gen.py debug.viz=true model.type=torch
yes | python nnsmith/cli/model_gen.py model.type=onnx
yes | python nnsmith/cli/model_gen.py debug.viz=true model.type=torch mgen.method=symbolic
yes | python nnsmith/cli/model_gen.py model.type=onnx mgen.method=symbolic
python nnsmith/cli/model_exec.py model.type=onnx backend.type=onnxruntime model.path=nnsmith_output/model.onnx
yes | python nnsmith/cli/model_gen.py model.type=tensorflow
yes | python nnsmith/cli/model_gen.py model.type=tensorflow mgen.method=symbolic
python nnsmith/cli/model_exec.py model.type=tensorflow backend.type=xla model.path=nnsmith_output/model/
- name: Test CLI [Concolic model_gen + model_exec]
run: |
yes | python nnsmith/cli/model_gen.py debug.viz=true model.type=torch mgen.method=concolic
yes | python nnsmith/cli/model_gen.py model.type=onnx mgen.method=concolic
python nnsmith/cli/model_exec.py model.type=onnx backend.type=onnxruntime model.path=nnsmith_output/model.onnx
yes | python nnsmith/cli/model_gen.py model.type=tensorflow mgen.method=concolic
python nnsmith/cli/model_exec.py model.type=tensorflow backend.type=xla model.path=nnsmith_output/model/
- name: Test CLI [fuzz]
run: |
Expand Down
5 changes: 4 additions & 1 deletion nnsmith/abstract/arith.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@

import z3

from nnsmith.error import SanityCheck
from nnsmith.error import ConstraintCheck, SanityCheck

ARITH_MAX_WIDTH: int = 64

Expand Down Expand Up @@ -163,6 +163,7 @@ def nnsmith_div(
if isinstance(left, z3.BitVecRef) or isinstance(right, z3.BitVecRef):
return z3.UDiv(left, right)
if isinstance(left, int) and isinstance(right, int):
ConstraintCheck.true(right != 0, "Div by zero")
return left // right
return left / right

Expand All @@ -173,6 +174,8 @@ def nnsmith_mod(
left, right = align_bvs(left, right)
if isinstance(left, z3.BitVecRef) or isinstance(right, z3.BitVecRef):
return z3.URem(left, right)
if isinstance(right, int):
ConstraintCheck.true(right != 0, "Mod by zero")
return left % right


Expand Down
17 changes: 12 additions & 5 deletions nnsmith/abstract/dtype.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ def short(self) -> str:
DType.int64: "i64",
DType.complex64: "c64",
DType.complex128: "c128",
DType.bool: "bool",
DType.bool: "b",
}[self]

@staticmethod
Expand All @@ -56,9 +56,12 @@ def from_str(s):
"i64": DType.int64,
"c64": DType.complex64,
"c128": DType.complex128,
"float16": DType.float16,
"float32": DType.float32,
"float64": DType.float64,
"uint8": DType.uint8,
"int8": DType.int8,
"int16": DType.int16,
"int32": DType.int32,
"int64": DType.int64,
"complex64": DType.complex64,
Expand Down Expand Up @@ -168,13 +171,17 @@ def sizeof(self) -> int:
}[self]


DTYPE_ALL = [
# "DTYPE_GEN*" means data types used for symbolic generation.
# "DTYPE_GEN_ALL" is surely a subset of all types but it is
# used to conservatively to avoid unsupported data types while
# applying nnsmith to various frameworks.
DTYPE_GEN_ALL = [
DType.float32,
DType.float64,
DType.int32,
DType.int64,
DType.bool,
]
DTYPE_NON_BOOLS = [dtype for dtype in DTYPE_ALL if dtype != DType.bool]
DTYPE_FLOATS = [DType.float32, DType.float64]
DTYPE_INTS = [DType.int32, DType.int64]
DTYPE_GEN_NON_BOOL = [dtype for dtype in DTYPE_GEN_ALL if dtype != DType.bool]
DTYPE_GEN_FLOATS = [DType.float32, DType.float64]
DTYPE_GEN_INTS = [DType.int32, DType.int64]
Loading