Added inputs and rules for xla apis

rules-tf/xla.reduce_precision/rule_1.py

@@ -0,0 +1,36 @@
+import numpy as np
+import torch 
+import tensorflow as tf
+
+from utils.defaults import MAX_N_DIM, MAX_SZ_DIM, MAX_SZ_NUM, list_of_available_dtypes, list_of_string_values_tf, np_dtype
+from z3 import *
+
+# exponent_bits must be non-negative (Rule 1)
+
+rule_1 = lambda s, v, n=False: (
+    s.add(Not(v["arg1_value"] >= 0) if n else
+          v["arg1_value"] >= 0)
+)
+
+def rule_1_func(arg1, solver=None, neg=False):
+    arg1 = next(iter(arg1.values()))
+
+    # Invariant learning phase
+    if not solver:
+        if not (isinstance(arg1, (int, np.integer)) and not isinstance(arg1, bool)):
+            return False
+
+        # Variable declarations
+        solver = Solver()
+        arg1_value = Int('arg1_value')
+
+        # Value assignments
+        solver.add(arg1_value == int(arg1))
+
+        # Constraints for rule 1
+        rule_1(solver, {'arg1_value': arg1_value})
+        return solver.check() == sat
+
+    # Fuzz input generation phase
+    else:
+        rule_1(solver, {'arg1_value': arg1['value']}, neg)

rules-tf/xla.reduce_precision/rule_11.py

@@ -0,0 +1,41 @@
+import numpy as np
+import torch 
+import tensorflow as tf
+
+from utils.defaults import MAX_N_DIM, MAX_SZ_DIM, MAX_SZ_NUM, list_of_available_dtypes, list_of_string_values_tf, np_dtype
+from z3 import *
+
+# exponent_bits or mantissa bits can be zero (Rule 11)
+
+rule_11 = lambda s, v, n=False: (
+    s.add(Not(Or(v["arg1_value"] == 0, v["arg2_value"] == 0)) if n else
+          Or(v["arg1_value"] == 0, v["arg2_value"] == 0))
+)
+
+def rule_11_func(arg1, arg2, solver=None, neg=False):
+    arg1 = next(iter(arg1.values()))
+    arg2 = next(iter(arg2.values()))
+
+    # Invariant learning phase
+    if not solver:
+        if not (isinstance(arg1, (int, np.integer)) and not isinstance(arg1, bool)):
+            return False
+        if not (isinstance(arg2, (int, np.integer)) and not isinstance(arg2, bool)):
+            return False
+
+        # Variable declarations
+        solver = Solver()
+        arg1_value = Int('arg1_value')
+        arg2_value = Int('arg2_value')
+
+        # Value assignments
+        solver.add(arg1_value == int(arg1))
+        solver.add(arg2_value == int(arg2))
+
+        # Constraints for rule 11
+        rule_11(solver, {'arg1_value': arg1_value, 'arg2_value': arg2_value})
+        return solver.check() == sat
+
+    # Fuzz input generation phase
+    else:
+        rule_11(solver, {'arg1_value': arg1['value'], 'arg2_value': arg2['value']}, neg)

rules-tf/xla.reduce_precision/rule_12.py

@@ -0,0 +1,46 @@
+import numpy as np
+import torch 
+import tensorflow as tf
+
+from utils.defaults import MAX_N_DIM, MAX_SZ_DIM, MAX_SZ_NUM, list_of_available_dtypes, list_of_string_values_tf, np_dtype
+from z3 import *
+
+# exponent_bits and mantissa_bits cannot be both zero if the input is a float16 (Rule 12)
+
+rule_12 = lambda s, v, n=False: (
+    s.add(Not(If(v["arg1_dtype"] == 6, Or(v["arg2_value"] > 0, v["arg3_value"] > 0), True)) if n else
+          If(v["arg1_dtype"] == 6, Or(v["arg2_value"] > 0, v["arg3_value"] > 0), True))
+)
+
+def rule_12_func(arg1, arg2, arg3, solver=None, neg=False):
+    arg1 = next(iter(arg1.values()))
+    arg2 = next(iter(arg2.values()))
+    arg3 = next(iter(arg3.values()))
+
+    # Invariant learning phase
+    if not solver:
+        if not isinstance(arg1, np.ndarray):
+            return False
+        if not (isinstance(arg2, (int, np.integer)) and not isinstance(arg2, bool)):
+            return False
+        if not (isinstance(arg3, (int, np.integer)) and not isinstance(arg3, bool)):
+            return False
+
+        # Variable declarations
+        solver = Solver()
+        arg1_dtype = Int('arg1_dtype')
+        arg2_value = Int('arg2_value')
+        arg3_value = Int('arg3_value')
+
+        # Value assignments
+        solver.add(arg1_dtype == list_of_available_dtypes.index(arg1.dtype))
+        solver.add(arg2_value == int(arg2))
+        solver.add(arg3_value == int(arg3))
+
+        # Constraints for rule 12
+        rule_12(solver, {'arg1_dtype': arg1_dtype, 'arg2_value': arg2_value, 'arg3_value': arg3_value})
+        return solver.check() == sat
+
+    # Fuzz input generation phase
+    else:
+        rule_12(solver, {'arg1_dtype': arg1['dtype'], 'arg2_value': arg2['value'], 'arg3_value': arg3['value']}, neg)

rules-tf/xla.reduce_precision/rule_13.py

@@ -0,0 +1,36 @@
+import numpy as np
+import torch 
+import tensorflow as tf
+
+from utils.defaults import MAX_N_DIM, MAX_SZ_DIM, MAX_SZ_NUM, list_of_available_dtypes, list_of_string_values_tf, np_dtype
+from z3 import *
+
+# exponent_bits cannot be greater than maximum allowed bits (Rule 13)
+
+rule_13 = lambda s, v, n=False: (
+    s.add(Not(v["arg1_value"] <= 63) if n else
+          v["arg1_value"] <= 63)
+)
+
+def rule_13_func(arg1, solver=None, neg=False):
+    arg1 = next(iter(arg1.values()))
+
+    # Invariant learning phase
+    if not solver:
+        if not (isinstance(arg1, (int, np.integer)) and not isinstance(arg1, bool)):
+            return False
+
+        # Variable declarations
+        solver = Solver()
+        arg1_value = Int('arg1_value')
+
+        # Value assignments
+        solver.add(arg1_value == int(arg1))
+
+        # Constraints for rule 13
+        rule_13(solver, {'arg1_value': arg1_value})
+        return solver.check() == sat
+
+    # Fuzz input generation phase
+    else:
+        rule_13(solver, {'arg1_value': arg1['value']}, neg)

rules-tf/xla.reduce_precision/rule_14.py

@@ -0,0 +1,36 @@
+import numpy as np
+import torch 
+import tensorflow as tf
+
+from utils.defaults import MAX_N_DIM, MAX_SZ_DIM, MAX_SZ_NUM, list_of_available_dtypes, list_of_string_values_tf, np_dtype
+from z3 import *
+
+# mantissa_bits cannot be greater than maximum allowed bits (Rule 14)
+
+rule_14 = lambda s, v, n=False: (
+    s.add(Not(v["arg1_value"] <= 63) if n else
+          v["arg1_value"] <= 63)
+)
+
+def rule_14_func(arg1, solver=None, neg=False):
+    arg1 = next(iter(arg1.values()))
+
+    # Invariant learning phase
+    if not solver:
+        if not (isinstance(arg1, (int, np.integer)) and not isinstance(arg1, bool)):
+            return False
+
+        # Variable declarations
+        solver = Solver()
+        arg1_value = Int('arg1_value')
+
+        # Value assignments
+        solver.add(arg1_value == int(arg1))
+
+        # Constraints for rule 14
+        rule_14(solver, {'arg1_value': arg1_value})
+        return solver.check() == sat
+
+    # Fuzz input generation phase
+    else:
+        rule_14(solver, {'arg1_value': arg1['value']}, neg)

rules-tf/xla.reduce_precision/rule_15.py

@@ -0,0 +1,46 @@
+import numpy as np
+import torch 
+import tensorflow as tf
+
+from utils.defaults import MAX_N_DIM, MAX_SZ_DIM, MAX_SZ_NUM, list_of_available_dtypes, list_of_string_values_tf, np_dtype
+from z3 import *
+
+# If operand is bool, then exponent_bits and mantissa_bits should be 0 (Rule 15)
+
+rule_15 = lambda s, v, n=False: (
+    s.add(Not(If(v["arg1_dtype"] == 0, And(v["arg2_value"] == 0, v["arg3_value"] == 0), True)) if n else
+          If(v["arg1_dtype"] == 0, And(v["arg2_value"] == 0, v["arg3_value"] == 0), True))
+)
+
+def rule_15_func(arg1, arg2, arg3, solver=None, neg=False):
+    arg1 = next(iter(arg1.values()))
+    arg2 = next(iter(arg2.values()))
+    arg3 = next(iter(arg3.values()))
+
+    # Invariant learning phase
+    if not solver:
+        if not isinstance(arg1, np.ndarray):
+            return False
+        if not (isinstance(arg2, (int, np.integer)) and not isinstance(arg2, bool)):
+            return False
+        if not (isinstance(arg3, (int, np.integer)) and not isinstance(arg3, bool)):
+            return False
+
+        # Variable declarations
+        solver = Solver()
+        arg1_dtype = Int('arg1_dtype')
+        arg2_value = Int('arg2_value')
+        arg3_value = Int('arg3_value')
+
+        # Value assignments
+        solver.add(arg1_dtype == list_of_available_dtypes.index(arg1.dtype))
+        solver.add(arg2_value == int(arg2))
+        solver.add(arg3_value == int(arg3))
+
+        # Constraints for rule 15
+        rule_15(solver, {'arg1_dtype': arg1_dtype, 'arg2_value': arg2_value, 'arg3_value': arg3_value})
+        return solver.check() == sat
+
+    # Fuzz input generation phase
+    else:
+        rule_15(solver, {'arg1_dtype': arg1['dtype'], 'arg2_value': arg2['value'], 'arg3_value': arg3['value']}, neg)

rules-tf/xla.reduce_precision/rule_16.py

@@ -0,0 +1,46 @@
+import numpy as np
+import torch 
+import tensorflow as tf
+
+from utils.defaults import MAX_N_DIM, MAX_SZ_DIM, MAX_SZ_NUM, list_of_available_dtypes, list_of_string_values_tf, np_dtype
+from z3 import *
+
+# If operand is complex, exponent_bits and mantissa_bits must be zero (Rule 16)
+
+rule_16 = lambda s, v, n=False: (
+    s.add(Not(If(Or(v["arg1_dtype"] == 9, v["arg1_dtype"] == 10), And(v["arg2_value"] == 0, v["arg3_value"] == 0), True)) if n else
+          If(Or(v["arg1_dtype"] == 9, v["arg1_dtype"] == 10), And(v["arg2_value"] == 0, v["arg3_value"] == 0), True))
+)
+
+def rule_16_func(arg1, arg2, arg3, solver=None, neg=False):
+    arg1 = next(iter(arg1.values()))
+    arg2 = next(iter(arg2.values()))
+    arg3 = next(iter(arg3.values()))
+
+    # Invariant learning phase
+    if not solver:
+        if not isinstance(arg1, np.ndarray):
+            return False
+        if not (isinstance(arg2, (int, np.integer)) and not isinstance(arg2, bool)):
+            return False
+        if not (isinstance(arg3, (int, np.integer)) and not isinstance(arg3, bool)):
+            return False
+
+        # Variable declarations
+        solver = Solver()
+        arg1_dtype = Int('arg1_dtype')
+        arg2_value = Int('arg2_value')
+        arg3_value = Int('arg3_value')
+
+        # Value assignments
+        solver.add(arg1_dtype == list_of_available_dtypes.index(arg1.dtype))
+        solver.add(arg2_value == int(arg2))
+        solver.add(arg3_value == int(arg3))
+
+        # Constraints for rule 16
+        rule_16(solver, {'arg1_dtype': arg1_dtype, 'arg2_value': arg2_value, 'arg3_value': arg3_value})
+        return solver.check() == sat
+
+    # Fuzz input generation phase
+    else:
+        rule_16(solver, {'arg1_dtype': arg1['dtype'], 'arg2_value': arg2['value'], 'arg3_value': arg3['value']}, neg)

rules-tf/xla.reduce_precision/rule_17.py

@@ -0,0 +1,46 @@
+import numpy as np
+import torch 
+import tensorflow as tf
+
+from utils.defaults import MAX_N_DIM, MAX_SZ_DIM, MAX_SZ_NUM, list_of_available_dtypes, list_of_string_values_tf, np_dtype
+from z3 import *
+
+# exponent_bits and mantissa_bits sum must be less than or equal to the total bits available in the float type (Rule 17)
+
+rule_17 = lambda s, v, n=False: (
+    s.add(Not(If(v["arg1_dtype"] == 6, v["arg2_value"] + v["arg3_value"] <= 11, If(v["arg1_dtype"] == 7, v["arg2_value"] + v["arg3_value"] <= 24, If(v["arg1_dtype"] == 8, v["arg2_value"] + v["arg3_value"] <= 53, True)))) if n else
+          If(v["arg1_dtype"] == 6, v["arg2_value"] + v["arg3_value"] <= 11, If(v["arg1_dtype"] == 7, v["arg2_value"] + v["arg3_value"] <= 24, If(v["arg1_dtype"] == 8, v["arg2_value"] + v["arg3_value"] <= 53, True))))
+)
+
+def rule_17_func(arg1, arg2, arg3, solver=None, neg=False):
+    arg1 = next(iter(arg1.values()))
+    arg2 = next(iter(arg2.values()))
+    arg3 = next(iter(arg3.values()))
+
+    # Invariant learning phase
+    if not solver:
+        if not isinstance(arg1, np.ndarray):
+            return False
+        if not (isinstance(arg2, (int, np.integer)) and not isinstance(arg2, bool)):
+            return False
+        if not (isinstance(arg3, (int, np.integer)) and not isinstance(arg3, bool)):
+            return False
+
+        # Variable declarations
+        solver = Solver()
+        arg1_dtype = Int('arg1_dtype')
+        arg2_value = Int('arg2_value')
+        arg3_value = Int('arg3_value')
+
+        # Value assignments
+        solver.add(arg1_dtype == list_of_available_dtypes.index(arg1.dtype))
+        solver.add(arg2_value == int(arg2))
+        solver.add(arg3_value == int(arg3))
+
+        # Constraints for rule 17
+        rule_17(solver, {'arg1_dtype': arg1_dtype, 'arg2_value': arg2_value, 'arg3_value': arg3_value})
+        return solver.check() == sat
+
+    # Fuzz input generation phase
+    else:
+        rule_17(solver, {'arg1_dtype': arg1['dtype'], 'arg2_value': arg2['value'], 'arg3_value': arg3['value']}, neg)

rules-tf/xla.reduce_precision/rule_18.py

@@ -0,0 +1,46 @@
+import numpy as np
+import torch 
+import tensorflow as tf
+
+from utils.defaults import MAX_N_DIM, MAX_SZ_DIM, MAX_SZ_NUM, list_of_available_dtypes, list_of_string_values_tf, np_dtype
+from z3 import *
+
+# If operand is integer, then exponent_bits and mantissa_bits must be 0 (Rule 18)
+
+rule_18 = lambda s, v, n=False: (
+    s.add(Not(If(And(1 <= v["arg1_dtype"], v["arg1_dtype"] <= 5), And(v["arg2_value"] == 0, v["arg3_value"] == 0), True)) if n else
+          If(And(1 <= v["arg1_dtype"], v["arg1_dtype"] <= 5), And(v["arg2_value"] == 0, v["arg3_value"] == 0), True))
+)
+
+def rule_18_func(arg1, arg2, arg3, solver=None, neg=False):
+    arg1 = next(iter(arg1.values()))
+    arg2 = next(iter(arg2.values()))
+    arg3 = next(iter(arg3.values()))
+
+    # Invariant learning phase
+    if not solver:
+        if not isinstance(arg1, np.ndarray):
+            return False
+        if not (isinstance(arg2, (int, np.integer)) and not isinstance(arg2, bool)):
+            return False
+        if not (isinstance(arg3, (int, np.integer)) and not isinstance(arg3, bool)):
+            return False
+
+        # Variable declarations
+        solver = Solver()
+        arg1_dtype = Int('arg1_dtype')
+        arg2_value = Int('arg2_value')
+        arg3_value = Int('arg3_value')
+
+        # Value assignments
+        solver.add(arg1_dtype == list_of_available_dtypes.index(arg1.dtype))
+        solver.add(arg2_value == int(arg2))
+        solver.add(arg3_value == int(arg3))
+
+        # Constraints for rule 18
+        rule_18(solver, {'arg1_dtype': arg1_dtype, 'arg2_value': arg2_value, 'arg3_value': arg3_value})
+        return solver.check() == sat
+
+    # Fuzz input generation phase
+    else:
+        rule_18(solver, {'arg1_dtype': arg1['dtype'], 'arg2_value': arg2['value'], 'arg3_value': arg3['value']}, neg)