<commit_before>import logging
l = logging.getLogger("claripy.backends.backend_concrete")

import z3
zTrue = z3.BoolVal(True)
zFalse = z3.BoolVal(False)

from ..backend import BackendError, Backend

class BackendConcrete(Backend):
    def __init__(self):
        Backend.__init__(self)
        self._make_raw_ops(set(backend_operations) - { 'BitVec' }, op_module=bv)
        self._make_raw_ops(backend_fp_operations, op_module=fp)
        self._op_raw_result['BitVec'] = self.BitVec

    def BitVec(self, name, size, result=None): #pylint:disable=W0613,R0201
        if result is None:
            l.debug("BackendConcrete can only handle BitVec when we are given a model")
            raise BackendError("BackendConcrete can only handle BitVec when we are given a model")
        if name not in result.model:
            l.debug("BackendConcrete needs variable %s in the model", name)
            raise BackendError("BackendConcrete needs variable %s in the model" % name)
        else:
            return result.model[name]

    def _size(self, e, result=None):
        if type(e) in { bool, long, int }:
            return None
        elif type(e) in { bv.BVV }:
            return e.size()
        elif isinstance(e, fp.FPV):
            return e.sort.length
        else:
            raise BackendError("can't get size of type %s" % type(e))

    def _name(self, e, result=None): #pylint:disable=unused-argument,no-self-use
        return None

    def _identical(self, a, b, result=None):
        if type(a) is bv.BVV and type(b) is bv.BVV and a.size() != b.size():
            return False
        else:
            return a == b

    def _convert(self, a, result=None):
        if type(a) in { int, long, float, bool, str, bv.BVV, fp.FPV, fp.RM, fp.FSort }:
            return a

        if not hasattr(a, '__module__') or a.__module__ != 'z3':
            raise BackendError("BackendConcrete got an unsupported type %s" % a.__class__)

        #if _backend_z3 is None:
        #   raise BackendError("can't convert z3 expressions when z3 is not in use")

        try:
            #if hasattr(_backend_z3, '_lock'):
            #   _backend_z3._lock.acquire() #pylint:disable=no-member

            if hasattr(a, 'as_long'): return bv.BVV(a.as_long(), a.size())
            elif isinstance(a, z3.FPRef):
                # TODO: don't replicate this code in backend_z3.py
                # this is really imprecise
                fp_mantissa = float(a.significand())
                fp_exp = float(a.exponent())
                value = fp_mantissa * (2 ** fp_exp)

                ebits = a.ebits()
                sbits = a.sbits()<commit_msg>Quick fix for FPRef bug<commit_after>import logging
l = logging.getLogger("claripy.backends.backend_concrete")

import z3
zTrue = z3.BoolVal(True)
zFalse = z3.BoolVal(False)

from ..backend import BackendError, Backend

class BackendConcrete(Backend):
    def __init__(self):
        Backend.__init__(self)
        self._make_raw_ops(set(backend_operations) - { 'BitVec' }, op_module=bv)
        self._make_raw_ops(backend_fp_operations, op_module=fp)
        self._op_raw_result['BitVec'] = self.BitVec

    def BitVec(self, name, size, result=None): #pylint:disable=W0613,R0201
        if result is None:
            l.debug("BackendConcrete can only handle BitVec when we are given a model")
            raise BackendError("BackendConcrete can only handle BitVec when we are given a model")
        if name not in result.model:
            l.debug("BackendConcrete needs variable %s in the model", name)
            raise BackendError("BackendConcrete needs variable %s in the model" % name)
        else:
            return result.model[name]

    def _size(self, e, result=None):
        if type(e) in { bool, long, int }:
            return None
        elif type(e) in { bv.BVV }:
            return e.size()
        elif isinstance(e, fp.FPV):
            return e.sort.length
        else:
            raise BackendError("can't get size of type %s" % type(e))

    def _name(self, e, result=None): #pylint:disable=unused-argument,no-self-use
        return None

    def _identical(self, a, b, result=None):
        if type(a) is bv.BVV and type(b) is bv.BVV and a.size() != b.size():
            return False
        else:
            return a == b

    def _convert(self, a, result=None):
        if type(a) in { int, long, float, bool, str, bv.BVV, fp.FPV, fp.RM, fp.FSort }:
            return a

        if not hasattr(a, '__module__') or a.__module__ != 'z3':
            raise BackendError("BackendConcrete got an unsupported type %s" % a.__class__)

        #if _backend_z3 is None:
        #   raise BackendError("can't convert z3 expressions when z3 is not in use")

        try:
            #if hasattr(_backend_z3, '_lock'):
            #   _backend_z3._lock.acquire() #pylint:disable=no-member

            if hasattr(a, 'as_long'): return bv.BVV(a.as_long(), a.size())
            elif isinstance(a, z3.FPNumRef):
                # TODO: don't replicate this code in backend_z3.py
                # this is really imprecise
                fp_mantissa = float(a.significand())
                fp_exp = float(a.exponent())
                value = fp_mantissa * (2 ** fp_exp)

                ebits = a.ebits()
                sbits = a.sbits()
{'fraction_non_alphanumeric': 0.10908406996426556, 'fraction_numerical': 0.007523039307880384, 'mean_word_length': 2.2446613788895666, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3729529', 'n_tokens_mistral': 1726, 'n_tokens_neox': 1678, 'n_words': 467}