<commit_before>#!/usr/bin/env python

import logging
import itertools

l = logging.getLogger("simuvex.plugins.symbolic_memory")

import claripy
from ..storage.memory import SimMemory
from ..storage.paged_memory import SimPagedMemory
from ..storage.memory_object import SimMemoryObject

DEFAULT_MAX_SEARCH = 8

class SimSymbolicMemory(SimMemory): #pylint:disable=abstract-method
    _CONCRETIZATION_STRATEGIES = [ 'symbolic', 'any', 'max', 'symbolic_nonzero', 'norepeats' ]
    _SAFE_CONCRETIZATION_STRATEGIES = [ 'symbolic' ]

    def __init__(self, backer=None, mem=None, memory_id="mem", repeat_min=None, repeat_constraints=None, repeat_expr=None, endness=None, abstract_backer=False):
        SimMemory.__init__(self, endness=endness, abstract_backer=abstract_backer)
        self.mem = SimPagedMemory(backer=backer) if mem is None else mem
        self.id = memory_id

        # for the norepeat stuff
        self._repeat_constraints = [ ] if repeat_constraints is None else repeat_constraints
        self._repeat_expr = repeat_expr
        self._repeat_granularity = 0x10000
        self._repeat_min = 0x13370000 if repeat_min is None else repeat_min

        # default strategies
        self._default_read_strategy = ['symbolic', 'any']
        self._default_write_strategy = [ 'max' ] #[ 'norepeats',  'any' ]
        self._default_symbolic_write_strategy = [ 'symbolic_nonzero', 'any' ]
        self._write_address_range = 1

    def set_state(self, s):
        SimMemory.set_state(self, s)
        self.mem.state = s

    def _ana_getstate(self):
        return self.__dict__.copy()

    #
    # Symbolicizing!
    #

    def make_symbolic(self, name, addr, length=None):
        '''
        Replaces length bytes, starting at addr, with a symbolic variable named
        name. Adds a constraint equaling that symbolic variable to the value
        previously at addr, and returns the variable.
        '''
        l.debug("making %s bytes symbolic", length)

        if isinstance(addr, str):
            addr, length = self.state.arch.registers[addr]
        else:
            if length is None:
                raise Exception("Unspecified length!")

        r = self.load(addr, length)

        v = self.get_unconstrained_bytes(name, r.size())
        self.store(addr, v)
        self.state.add_constraints(r == v)
        l.debug("... eq constraints: %s", r == v)
        return v

    #
    # Address concretization
    #

    def _symbolic_size_range(self, size):
        max_size = self.state.se.max_int(size)
        min_size = self.state.se.min_int(size)

        if min_size > self._maximum_symbolic_size:
            self.state.log.add_event('memory_limit', message="Symbolic size %d outside of allowable limits" % min_size, size=size)
            if options.BEST_EFFORT_MEMORY_STORING not in self.state.options:
                raise SimMemoryLimitError("Symbolic size %d outside of allowable limits" % min_size)
            else:
                min_size = self._maximum_symbolic_size

        return min_size, min(max_size, self._maximum_symbolic_size)

    def _concretize_strategy(self, v, s, limit):
        r = None
        #if s == "norepeats_simple":
        #    if self.state.se.solution(v, self._repeat_min):
        #        l.debug("... trying super simple method.")
        #        r = [ self._repeat_min ]
        #        self._repeat_min += self._repeat_granularity
        #elif s == "norepeats_range":
        #    l.debug("... trying ranged simple method.")
        #    r = [ self.state.se.any_int(v, extra_constraints = [ v > self._repeat_min, v < self._repeat_min + self._repeat_granularity ]) ]
        #    self._repeat_min += self._repeat_granularity
        #elif s == "norepeats_min":
        #    l.debug("... just getting any value.")
        #    r = [ self.state.se.any_int(v, extra_constraints = [ v > self._repeat_min ]) ]
        #    self._repeat_min = r[0] + self._repeat_granularity
        if s == "norepeats":
            if self._repeat_expr is None:
                self._repeat_expr = self.get_unconstrained_bytes("%s_repeat" % self.id, self.state.arch.bits)

            c = self.state.se.any_int(v, extra_constraints=self._repeat_constraints + [ v == self._repeat_expr ])
            self._repeat_constraints.append(self._repeat_expr != c)
            r = [ c ]
        elif s == "symbolic":
            # if the address concretizes to less than the threshold of values, try to keep it symbolic
            mx = self.state.se.max_int(v)
            mn = self.state.se.min_int(v)

            l.debug("... range is (%#x, %#x)", mn, mx)
            if mx - mn < limit:
                l.debug("... generating %d addresses", limit)
                r = self.state.se.any_n_int(v, limit)
                l.debug("... done, got %d", len(r))
        elif s == "symbolic_nonzero":
            # if the address concretizes to less than the threshold of values, try to keep it symbolic
            mx = self.state.se.max_int(v, extra_constraints=[v != 0])
            mn = self.state.se.min_int(v, extra_constraints=[v != 0])

            l.debug("... range is (%#x, %#x)", mn, mx)
            if mx - mn < limit:
                l.debug("... generating %d addresses", limit)
                r = self.state.se.any_n_int(v, limit)
                l.debug("... done, got %d", len(r))
        elif s == "any":
            r = [self.state.se.any_int(v)]
        elif s == "max":
            r = [self.state.se.max_int(v)]

        return r

    def _concretize_addr(self, v, strategy, limit):
        # if there's only one option, let's do it
        if not self.state.se.symbolic(v):
            l.debug("... concrete value")
            return [ self.state.se.any_int(v) ]

        if not self.state.satisfiable():
            raise SimMemoryAddressError("Trying to concretize with unsat constraints.")

        l.debug("... concretizing address with limit %d", limit)

        for s in strategy:<commit_msg>don't spend time explicitly checking for state satisfiability<commit_after>#!/usr/bin/env python

import logging
import itertools

l = logging.getLogger("simuvex.plugins.symbolic_memory")

import claripy
from ..storage.memory import SimMemory
from ..storage.paged_memory import SimPagedMemory
from ..storage.memory_object import SimMemoryObject

DEFAULT_MAX_SEARCH = 8

class SimSymbolicMemory(SimMemory): #pylint:disable=abstract-method
    _CONCRETIZATION_STRATEGIES = [ 'symbolic', 'any', 'max', 'symbolic_nonzero', 'norepeats' ]
    _SAFE_CONCRETIZATION_STRATEGIES = [ 'symbolic' ]

    def __init__(self, backer=None, mem=None, memory_id="mem", repeat_min=None, repeat_constraints=None, repeat_expr=None, endness=None, abstract_backer=False):
        SimMemory.__init__(self, endness=endness, abstract_backer=abstract_backer)
        self.mem = SimPagedMemory(backer=backer) if mem is None else mem
        self.id = memory_id

        # for the norepeat stuff
        self._repeat_constraints = [ ] if repeat_constraints is None else repeat_constraints
        self._repeat_expr = repeat_expr
        self._repeat_granularity = 0x10000
        self._repeat_min = 0x13370000 if repeat_min is None else repeat_min

        # default strategies
        self._default_read_strategy = ['symbolic', 'any']
        self._default_write_strategy = [ 'max' ] #[ 'norepeats',  'any' ]
        self._default_symbolic_write_strategy = [ 'symbolic_nonzero', 'any' ]
        self._write_address_range = 1

    def set_state(self, s):
        SimMemory.set_state(self, s)
        self.mem.state = s

    def _ana_getstate(self):
        return self.__dict__.copy()

    #
    # Symbolicizing!
    #

    def make_symbolic(self, name, addr, length=None):
        '''
        Replaces length bytes, starting at addr, with a symbolic variable named
        name. Adds a constraint equaling that symbolic variable to the value
        previously at addr, and returns the variable.
        '''
        l.debug("making %s bytes symbolic", length)

        if isinstance(addr, str):
            addr, length = self.state.arch.registers[addr]
        else:
            if length is None:
                raise Exception("Unspecified length!")

        r = self.load(addr, length)

        v = self.get_unconstrained_bytes(name, r.size())
        self.store(addr, v)
        self.state.add_constraints(r == v)
        l.debug("... eq constraints: %s", r == v)
        return v

    #
    # Address concretization
    #

    def _symbolic_size_range(self, size):
        max_size = self.state.se.max_int(size)
        min_size = self.state.se.min_int(size)

        if min_size > self._maximum_symbolic_size:
            self.state.log.add_event('memory_limit', message="Symbolic size %d outside of allowable limits" % min_size, size=size)
            if options.BEST_EFFORT_MEMORY_STORING not in self.state.options:
                raise SimMemoryLimitError("Symbolic size %d outside of allowable limits" % min_size)
            else:
                min_size = self._maximum_symbolic_size

        return min_size, min(max_size, self._maximum_symbolic_size)

    def _concretize_strategy(self, v, s, limit):
        r = None
        #if s == "norepeats_simple":
        #    if self.state.se.solution(v, self._repeat_min):
        #        l.debug("... trying super simple method.")
        #        r = [ self._repeat_min ]
        #        self._repeat_min += self._repeat_granularity
        #elif s == "norepeats_range":
        #    l.debug("... trying ranged simple method.")
        #    r = [ self.state.se.any_int(v, extra_constraints = [ v > self._repeat_min, v < self._repeat_min + self._repeat_granularity ]) ]
        #    self._repeat_min += self._repeat_granularity
        #elif s == "norepeats_min":
        #    l.debug("... just getting any value.")
        #    r = [ self.state.se.any_int(v, extra_constraints = [ v > self._repeat_min ]) ]
        #    self._repeat_min = r[0] + self._repeat_granularity
        if s == "norepeats":
            if self._repeat_expr is None:
                self._repeat_expr = self.get_unconstrained_bytes("%s_repeat" % self.id, self.state.arch.bits)

            c = self.state.se.any_int(v, extra_constraints=self._repeat_constraints + [ v == self._repeat_expr ])
            self._repeat_constraints.append(self._repeat_expr != c)
            r = [ c ]
        elif s == "symbolic":
            # if the address concretizes to less than the threshold of values, try to keep it symbolic
            mx = self.state.se.max_int(v)
            mn = self.state.se.min_int(v)

            l.debug("... range is (%#x, %#x)", mn, mx)
            if mx - mn < limit:
                l.debug("... generating %d addresses", limit)
                r = self.state.se.any_n_int(v, limit)
                l.debug("... done, got %d", len(r))
        elif s == "symbolic_nonzero":
            # if the address concretizes to less than the threshold of values, try to keep it symbolic
            mx = self.state.se.max_int(v, extra_constraints=[v != 0])
            mn = self.state.se.min_int(v, extra_constraints=[v != 0])

            l.debug("... range is (%#x, %#x)", mn, mx)
            if mx - mn < limit:
                l.debug("... generating %d addresses", limit)
                r = self.state.se.any_n_int(v, limit)
                l.debug("... done, got %d", len(r))
        elif s == "any":
            r = [self.state.se.any_int(v)]
        elif s == "max":
            r = [self.state.se.max_int(v)]

        return r

    def _concretize_addr(self, v, strategy, limit):
        # if there's only one option, let's do it
        if not self.state.se.symbolic(v):
            l.debug("... concrete value")
            return [ self.state.se.any_int(v) ]

        l.debug("... concretizing address with limit %d", limit)

        for s in strategy:
{'fraction_non_alphanumeric': 0.11517043536955789, 'fraction_numerical': 0.0033749578130273373, 'mean_word_length': 2.316452154448797, 'pattern_counts': {'":': 16, '<': 9, '<?xml version=': 0, '>': 9, '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': '2995952', 'n_tokens_mistral': 3796, 'n_tokens_neox': 3693, 'n_words': 894}