Merge branch 'wip/z3_update'

Author: rhelmot

claripy/ast/fp.py

@@ -132,6 +132,8 @@ def _fp_cmp_check(a, b):
 fpGEQ = operations.op('fpGEQ', (FP, FP), Bool, bound=False, extra_check=_fp_cmp_check)
 fpLT = operations.op('fpLT', (FP, FP), Bool, bound=False, extra_check=_fp_cmp_check)
 fpLEQ = operations.op('fpLEQ', (FP, FP), Bool, bound=False, extra_check=_fp_cmp_check)
+fpIsNaN = operations.op('fpIsNaN', (FP,), Bool, bound=False)
+fpIsInf = operations.op('fpIsInf', (FP,), Bool, bound=False)
 
 #
 # unbound floating point arithmetic
@@ -173,3 +175,6 @@ def _fp_binop_length(rm, a, b): #pylint:disable=unused-argument
 FP.__rmul__ = operations.reversed_op(FP.__mul__)
 FP.__rdiv__ = operations.reversed_op(FP.__div__)
 FP.__rtruediv__ = operations.reversed_op(FP.__div__)
+
+FP.isNaN = fpIsNaN
+FP.isInf = fpIsInf

claripy/backend_object.py

@@ -15,4 +15,3 @@ def to_claripy(self):
         """
 
         return self
-

claripy/backends/backend_concrete.py

@@ -39,7 +39,7 @@ def BVV(value, size):
         return bv.BVV(value, size)
 
     @staticmethod
-    def StringV(value, size):
+    def StringV(value, size): # pylint: disable=unused-argument
         if not value:
             raise BackendError("can't handle empty Strings")
         return strings.StringV(value)
@@ -85,8 +85,7 @@ def convert(self, expr):
     def _If(self, b, t, f): #pylint:disable=no-self-use,unused-argument
         if not isinstance(b, bool):
             raise BackendError("BackendConcrete can't handle non-bool condition in If.")
-        else:
-            return t if b else f
+        return t if b else f
 
     def _size(self, e):
         if isinstance(e, (bool, numbers.Number)):
@@ -125,7 +124,7 @@ def _abstract(self, e): #pylint:disable=no-self-use
         elif isinstance(e, fp.FPV):
             return FPV(e.value, e.sort)
         elif isinstance(e, strings.StringV):
-            return StringV(e.value) 
+            return StringV(e.value)
         else:
             raise BackendError("Couldn't abstract object of type {}".format(type(e)))
 
@@ -141,12 +140,14 @@ def _cardinality(self, b):
     def _to_primitive(expr):
         if isinstance(expr, bv.BVV):
             return expr.value
-        if isinstance(expr, fp.FPV):
+        elif isinstance(expr, fp.FPV):
             return expr.value
-        if isinstance(expr, bool):
+        elif isinstance(expr, bool):
             return expr
-        if isinstance(expr, numbers.Number):
+        elif isinstance(expr, numbers.Number):
             return expr
+        else:
+            raise BackendError("idk how to turn this into a primitive")
 
     def _eval(self, expr, n, extra_constraints=(), solver=None, model_callback=None):
         if not all(extra_constraints):

claripy/backends/backend_z3.py

@@ -24,6 +24,11 @@
 except ImportError:
     _is_pypy = False
 
+def z3_expr_to_smt2(f, status="unknown", name="benchmark", logic=""):
+      # from https://stackoverflow.com/a/14629021/9719920
+      v = (z3.Ast * 0)()
+      return z3.Z3_benchmark_to_smtlib_string(f.ctx_ref(), name, logic, status, "", 0, v, f.as_ast())
+
 def _add_memory_pressure(p):
     """
     PyPy's garbage collector is not aware of memory uses happening inside native code. When performing memory-intensive
@@ -46,6 +51,9 @@ def _add_memory_pressure(p):
 
 supports_fp = hasattr(z3, 'fpEQ')
 
+# you can toggle this flag if you want. I don't think it matters
+#z3.set_param('rewriter.hi_fp_unspecified', 'true')
+
 #
 # Utility functions
 #
@@ -69,18 +77,8 @@ def raw_caller(*args, **kwargs):
     return raw_caller
 
 def _z3_decl_name_str(ctx, decl):
-    # reimplementation of Z3_get_symbol_string to not try to unicode-decode
-    lib = z3.lib()
-
-    decl_name = lib.Z3_get_decl_name(ctx, decl)
-    err = lib.Z3_get_error_code(ctx)
-    if err != z3.Z3_OK:
-        raise z3.Z3Exception(lib.Z3_get_error_msg(ctx, err))
-
-    symbol_name = lib.Z3_get_symbol_string(ctx, decl_name)
-    err = lib.Z3_get_error_code(ctx)
-    if err != z3.Z3_OK:
-        raise z3.Z3Exception(z3.lib().Z3_get_error_msg(ctx, err))
+    decl_name = z3.Z3_get_decl_name(ctx, decl)
+    symbol_name = z3.Z3_get_symbol_string_bytes(ctx, decl_name)
     return symbol_name
 
 
@@ -562,20 +560,54 @@ def _abstract_to_primitive(self, ctx, ast):
         op_name = op_map[z3_op_nums[decl_num]]
 
         if op_name == 'BitVecVal':
-            if z3.Z3_get_numeral_uint64(ctx, ast, self._c_uint64_p):
-                return self._c_uint64_p.contents.value
-            else:
-                bv_num = int(z3.Z3_get_numeral_string(ctx, ast))
-                return bv_num
+            return self._abstract_bv_val(ctx, ast)
         elif op_name == 'True':
             return True
         elif op_name == 'False':
             return False
         elif op_name in ('FPVal', 'MinusZero', 'MinusInf', 'PlusZero', 'PlusInf', 'NaN'):
             return self._abstract_fp_val(ctx, ast, op_name)
+        elif op_name == 'Concat':
+            # Quirk in how z3 might handle NaN encodings - it will not give us a fully evaluated model
+            # https://github.com/Z3Prover/z3/issues/518
+            # this case will be triggered if the z3 rewriter.hi_fp_unspecified is set to true
+            nargs = z3.Z3_get_app_num_args(ctx, ast)
+            res = 0
+            for i in range(nargs):
+                arg_ast = z3.Z3_get_app_arg(ctx, ast, i)
+                arg_decl = z3.Z3_get_app_decl(ctx, arg_ast)
+                arg_decl_num = z3.Z3_get_decl_kind(ctx, arg_decl)
+                arg_size = z3.Z3_get_bv_sort_size(ctx, z3.Z3_get_sort(ctx, arg_ast))
+
+                neg = False
+                if arg_decl_num == z3.Z3_OP_BNEG:
+                    arg_ast = z3.Z3_get_app_arg(ctx, arg_ast, 0)
+                    arg_decl = z3.Z3_get_app_decl(ctx, arg_ast)
+                    arg_decl_num = z3.Z3_get_decl_kind(ctx, arg_decl)
+                    neg = True
+                if arg_decl_num != z3.Z3_OP_BNUM:
+                    raise BackendError("Weird z3 model")
+
+                arg_int = self._abstract_bv_val(ctx, arg_ast)
+                if neg:
+                    arg_int = (1<<arg_size)-arg_int
+                res <<= arg_size
+                res |= arg_int
+            return res
+        elif op_name == 'fpToIEEEBV':
+            # Another quirk in the way z3 might handle nan encodings. see above
+            # this case will be triggered if the z3 rewriter.hi_fp_unspecified is set to false
+            arg_ast = z3.Z3_get_app_arg(ctx, ast, 0)
+            return self._abstract_fp_encoded_val(ctx, arg_ast)
         else:
             raise BackendError("Unable to abstract Z3 object to primitive")
 
+    def _abstract_bv_val(self, ctx, ast):
+        if z3.Z3_get_numeral_uint64(ctx, ast, self._c_uint64_p):
+            return self._c_uint64_p.contents.value
+        else:
+            return int(z3.Z3_get_numeral_string(ctx, ast))
+
     def _abstract_fp_val(self, ctx, ast, op_name):
         if op_name == 'FPVal':
             # TODO: do better than this
@@ -599,6 +631,47 @@ def _abstract_fp_val(self, ctx, ast, op_name):
         else:
             raise BackendError("Called _abstract_fp_val with unknown type")
 
+    def _abstract_fp_encoded_val(self, ctx, ast):
+        decl = z3.Z3_get_app_decl(ctx, ast)
+        decl_num = z3.Z3_get_decl_kind(ctx, decl)
+        op_name = op_map[z3_op_nums[decl_num]]
+        sort = z3.Z3_get_sort(ctx, ast)
+        ebits = z3.Z3_fpa_get_ebits(ctx, sort)
+        sbits = z3.Z3_fpa_get_sbits(ctx, sort) - 1  # includes sign bit
+
+        if op_name == 'FPVal':
+            # TODO: do better than this
+            fp_mantissa = int(z3.Z3_fpa_get_numeral_significand_string(ctx, ast))
+            fp_exp = int(z3.Z3_fpa_get_numeral_exponent_string(ctx, ast, True))
+            fp_sign_c = ctypes.c_int()
+            z3.Z3_fpa_get_numeral_sign(ctx, ast, ctypes.byref(fp_sign_c))
+            fp_sign = 1 if fp_sign_c.value != 0 else 0
+        elif op_name == 'MinusZero':
+            fp_sign = 1
+            fp_exp = 0
+            fp_mantissa = 0
+        elif op_name == 'MinusInf':
+            fp_sign = 1
+            fp_exp = (1<<ebits) - 1
+            fp_mantissa = 0
+        elif op_name == 'PlusZero':
+            fp_sign = 0
+            fp_exp = 0
+            fp_mantissa = 0
+        elif op_name == 'PlusInf':
+            fp_sign = 0
+            fp_exp = (1<<ebits) - 1
+            fp_mantissa = 0
+        elif op_name == 'NaN':
+            fp_sign = 0
+            fp_exp = (1<<ebits) - 1
+            fp_mantissa = 1
+        else:
+            raise BackendError("Called _abstract_fp_val with unknown type")
+
+        value = (fp_sign << (ebits + sbits)) | (fp_exp << sbits) | fp_mantissa
+        return value
+
     def solver(self, timeout=None):
         if not self.reuse_z3_solver or getattr(self._tls, 'solver', None) is None:
             s = z3.Solver(ctx=self._context)
@@ -1047,6 +1120,14 @@ def _op_raw_fpGEQ(self, a, b):
     def _op_raw_fpEQ(self, a, b):
         return z3.BoolRef(z3.Z3_mk_fpa_eq(self._context.ref(), a.as_ast(), b.as_ast()), self._context)
 
+    @condom
+    def _op_raw_fpIsNaN(self, a):
+        return z3.BoolRef(z3.Z3_mk_fpa_is_nan(self._context.ref(), a.as_ast()), self._context)
+
+    @condom
+    def _op_raw_fpIsInf(self, a):
+        return z3.BoolRef(z3.Z3_mk_fpa_is_inf(self._context.ref(), a.as_ast()), self._context)
+
     @condom
     def _op_raw_fpFP(self, sgn, exp, sig):
         return z3.FPRef(z3.Z3_mk_fpa_fp(self._context.ref(), sgn.ast, exp.ast, sig.ast), self._context)

claripy/fp.py

@@ -443,4 +443,16 @@ def fpDiv(_rm, a, b):
     """
     return a / b
 
+def fpIsNaN(x):
+    """
+    Checks whether the argument is a floating point NaN.
+    """
+    return math.isnan(x)
+
+def fpIsInf(x):
+    """
+    Checks whether the argument is a floating point infinity.
+    """
+    return math.isinf(x)
+
 from .bv import BVV, Concat

claripy/operations.py

@@ -162,10 +162,10 @@ def str_extract_check(start_idx, count, str_val):
     else:
         return True, ""
 
-def str_extract_length_calc(start_idx, count, str_val):
+def str_extract_length_calc(start_idx, count, str_val): # pylint: diable=unused-argument
     return count
 
-def int_to_str_length_calc(int_val):
+def int_to_str_length_calc(int_val): # pylint: disable=unused-argument
     return ast.String.MAX_LENGTH
 
 def str_replace_check(*args):
@@ -174,7 +174,7 @@ def str_replace_check(*args):
         return False, "The pattern that has to be replaced is longer than the string itself"
     return True, ""
 
-def substr_length_calc(start_idx, count, strval):
+def substr_length_calc(start_idx, count, strval): # pylint: disable=unused-argument
     # FIXME: How can I get the value of a concrete object without a solver
     return strval.string_length if not count.concrete else count.args[0]
 
@@ -200,10 +200,10 @@ def str_replace_length_calc(*args):
 def strlen_bv_size_calc(s, bitlength):
     return bitlength
 
-def strindexof_bv_size_calc(s1, s2, start_idx, bitlength):
+def strindexof_bv_size_calc(s1, s2, start_idx, bitlength): # pylint: disable=unused-argument
     return bitlength
 
-def strtoint_bv_size_calc(s, bitlength):
+def strtoint_bv_size_calc(s, bitlength): # pylint: disable=unused-argument
     return bitlength
 
 #
@@ -312,7 +312,7 @@ def strtoint_bv_size_calc(s, bitlength):
 
 backend_fp_operations = {
     'FPS', 'fpToFP', 'fpToIEEEBV', 'fpFP', 'fpToSBV', 'fpToUBV',
-    'fpNeg', 'fpSub', 'fpAdd', 'fpMul', 'fpDiv', 'fpAbs'
+    'fpNeg', 'fpSub', 'fpAdd', 'fpMul', 'fpDiv', 'fpAbs', 'fpIsNaN', 'fpIsInf',
 } | backend_fp_cmp_operations
 
 backend_strings_operations = {

claripy/simplifications.py

@@ -542,9 +542,18 @@ def bitwise_xor_simplifier(a, b, *args):
         def _flattening_filter(args):
             # since a ^ a == 0, we can safely remove those from args
             # this procedure is done carefully in order to keep the ordering of arguments
-            ctr = collections.Counter(args)
-            unique_args = set(k.cache_key for k in ctr if ctr[k] % 2 != 0)
-            return tuple([ arg for arg in args if arg.cache_key in unique_args ])
+            ctr = collections.Counter(arg.cache_key for arg in args)
+            res = []
+            seen = set()
+            for arg in args:
+                if ctr[arg.cache_key] % 2 == 0:
+                    continue
+                l1 = len(seen)
+                seen.add(arg.cache_key)
+                l2 = len(seen)
+                if l1 != l2:
+                    res.append(arg)
+            return tuple(res)
 
         return SimplificationManager._flatten_simplifier('__xor__', _flattening_filter, a, b, *args, initial_value=ast.all_operations.BVV(0, a.size()))
 

setup.py

@@ -16,7 +16,7 @@
     python_requires='>=3.5',
     packages=packages,
     install_requires=[
-        'z3-solver==4.5.1.0.post2',
+        'z3-solver>=4.8.5.0',
         'future',
         'cachetools',
         'pysmt',

tests/test_solver.py

@@ -1,5 +1,6 @@
 import claripy
 import nose
+import math
 
 import logging
 l = logging.getLogger('claripy.test.solver')
@@ -559,9 +560,27 @@ def test_zero_division_in_cache_mixin():
     s.add(denum == 3)
     assert not s.satisfiable()
 
+def test_nan():
+    a = claripy.FPS('a', claripy.FSORT_FLOAT)
+    b = claripy.BVS('b', 32)
 
-if __name__ == '__main__':
+    s1 = claripy.Solver()
+    s1.add((a + 1).isNaN())
+    res = s1.eval(a, 1)[0]
+    assert math.isnan(res)
+
+    s2 = claripy.Solver()
+    s2.add(b.raw_to_fp().isNaN())
+    res = s2.eval(b, 1)[0]
+    assert res & 0xff800000 == 0x7f800000 and res & 0x007fffff != 0
+
+    s3 = claripy.Solver()
+    s3.add(a.isNaN())
+    res = s3.eval(a.raw_to_bv(), 1)[0]
+    assert res & 0xff800000 == 0x7f800000 and res & 0x007fffff != 0
 
+
+if __name__ == '__main__':
     for fparams in test_unsat_core():
         fparams[0](*fparams[1:])
 
@@ -584,3 +603,4 @@ def test_zero_division_in_cache_mixin():
         fparams[0](*fparams[1:])
     test_composite_solver()
     test_zero_division_in_cache_mixin()
+    test_nan()