<commit_before>#!/usr/bin/env python
import z3
import s_value
import random
import copy
import pdb
import itertools

import logging


logging.basicConfig()
l = logging.getLogger("s_memory")
addr_mem_counter = 0
var_mem_counter = 0

l.setLevel(logging.DEBUG)

class Memory:
    def __init__(self, initial=None, sys=None):
        #TODO: copy-on-write behaviour
        self.__mem = copy.copy(initial) if ( initial != None) else {}
        self.__limit = 1024
        self.__freemem = [(0, (2**64) - 1)]
        self.__max_mem = 2**64
        self.__sys = sys if (sys != None) else 8


    def store(self, dst, cnt, constraints):
        if len(self.__mem) == self.__max_mem:
            raise Exception("Memory is full.")

        v = s_value.Value(dst, constraints)
        r = ( v.min, v.max )
        ret = []

        if v.max == v.min:
            addr = v.min
        else:
            s = z3.Solver()
            con = False

            for i in range(0, len(self.__freemem)):
                con = z3.Or(z3.And(z3.UGE(dst, self.__freemem[i][0]), z3.ULE(dst, self.__freemem[i][1])), con)

            con = z3.simplify(con)
            if con == True: #it is always satisfiable%
                #TODO: pick up one random instead
                addr = (long(self.__mem.keys()[-1]) + 1) if len(self.__mem.keys()) != 0 else 0
                ret = [dst == addr]
            else:
                s.add(con)
                if s.check() == z3.unsat:
                    raise Exception("Unable to store new values in memory.")
                addr = s.model().get_interp(dst)
                ret = [dst == addr]

        for off in range(0, cnt.size() / 8):
            self.__mem[(addr + off)] = z3.Extract((off << 3) + 7, (off << 3), cnt)

        keys = [ -1 ] + self.__mem.keys() + [ 2**64 ]
        self.__freemem = [ j for j in [ ((keys[i] + 1, keys[i+1] - 1) if keys[i+1] - keys[i] > 1 else ()) for i in range(len(keys)-1) ] if j ]

        return ret

    #Load expressions from memory
    def load(self, dst, size, constraints=None):
        global addr_mem_counter
        global var_mem_counter

        if len(self.__mem) == 0:
            var = z3.BitVec("mem_%s" %(var_mem_counter), size)
            var_mem_counter += 1
            return var, []

        expr = False
        ret = None

        size_b = size >> 3
        v = s_value.Value(dst, constraints)
        r = ( v.min, v.max )

        if abs(v.max - v.min) <= self.__limit:
            w_k = range(v.min, v.max)
            w_k.append(v.max)
            p_k = list(set(w_k) & set(self.__mem.keys()))

            if len(p_k) == 0:
                l.debug("Loading operation outside its boundaries, symbolic variable found")
                expr = z3.BitVec("mem_%s" %(var_mem_counter), size)
                var_mem_counter += 1
            else:
                var = z3.BitVec("%s_addr_%s" %(dst, addr_mem_counter), self.__sys)
                addr_mem_counter += 1

                # specific read
                if len(p_k)/size_b == 0:
                    addr = p_k[0]
                    expr = z3.Concat(*[ self.__mem[addr + i] for i in range( 0, size_b)])
                    expr = z3.simplify(expr)
                else:
                    try:
                        for cnt in range(0, len(p_k)/size_b):
                            cnc = z3.Concat(*[ self.__mem[p_k[i + (cnt*size_b)]] for i in range( 0, size_b)])
                            new_expr = z3.Or(var == cnc, expr)
                            expr = z3.simplify(new_expr)
                    except:
                        l.debug("Loading not mutiple of %d" % size_b)
            ret = expr, []
        else:
            pos = range(0, len(self.__mem.keys()) / size_b)
            addr = random.choice(pos)
            cnc = z3.Concat(*[ self.__mem[(addr*size_b) + i] for i in range( 0, size_b)])
            cnc = z3.simplify(cnc)
            pdb.set_trace()
            ret = cnc, [dst == addr]

        return ret

    def get_bit_address(self):
        return self.__sys

    #TODO: copy-on-write behaviour
    def copy(self):
        return copy.copy(self)<commit_msg>load completed<commit_after>#!/usr/bin/env python
import z3
import s_value
import random
import copy
import pdb
import collections
import logging


logging.basicConfig()
l = logging.getLogger("s_memory")
addr_mem_counter = 0
var_mem_counter = 0

l.setLevel(logging.DEBUG)

def default_mem_value():
    global var_mem_counter
    var = z3.BitVec("mem_%d" %var_mem_counter, 8)
    var_mem_counter += 1
    return var

class Memory:

    def __init__(self, initial=None, sys=None):
        #TODO: copy-on-write behaviour
        self.__mem = copy.copy(initial) if ( initial != None) else collections.defaultdict(default_mem_value)
        self.__limit = 1024
        self.__bits = sys if (sys != None) else 64
        self.__max_mem = 2**self.__bits
        self.__freemem = [(0, self.__max_mem - 1)]


    def store(self, dst, cnt, constraints):
        if len(self.__mem) + cnt.size() >= self.__max_mem:
            raise Exception("Memory is full.")

        v = s_value.Value(dst, constraints)
        r = ( v.min, v.max )
        ret = []

        if v.max == v.min:
            addr = v.min
        else:
            s = z3.Solver()
            con = False

            for i in range(0, len(self.__freemem)):
                con = z3.Or(z3.And(z3.UGE(dst, self.__freemem[i][0]), z3.ULE(dst, self.__freemem[i][1])), con)

            con = z3.simplify(con)
            if con == True: # if it is always satisfiable%
                #TODO: pick up one random instead
                addr = (long(self.__mem.keys()[-1]) + 1) if len(self.__mem.keys()) != 0 else 0
                ret = [dst == addr]
            else:
                s.add(con)
                if s.check() == z3.unsat:
                    raise Exception("Unable to store new values in memory.")
                addr = s.model().get_interp(dst)
                ret = [dst == addr]

        for off in range(0, cnt.size() / 8):
            self.__mem[(addr + off)] = z3.Extract((off << 3) + 7, (off << 3), cnt)

        keys = [ -1 ] + self.__mem.keys() + [ self.__max_mem ]
        self.__freemem = [ j for j in [ ((keys[i] + 1, keys[i+1] - 1) if keys[i+1] - keys[i] > 1 else ()) for i in range(len(keys)-1) ] if j ]

        return ret

    #Load expressions from memory
    def load(self, dst, size, constraints=None):
        global addr_mem_counter
        global var_mem_counter

        if len(self.__mem) == 0:
            var = z3.BitVec("mem_%s" %(var_mem_counter), size)
            var_mem_counter += 1
            return var, []

        expr = False
        ret = None

        size_b = size >> 3
        v = s_value.Value(dst, constraints)
        r = ( v.min, v.max )

        # specific read
        if v.min == v.max:
            addr = v.min
            expr = self.__mem[addr] if (size_b == 1) else z3.Concat(*[self.__mem[addr + i] for i in range( 0, size_b)])
            expr = z3.simplify(expr)
            ret = expr, []

        elif abs(v.max - v.min) <= self.__limit:
            w_k = range(v.min, v.max)
            w_k.append(v.max)
            p_k = list(set(w_k) & set(self.__mem.keys()))

            if len(p_k) == 0:
                l.debug("Loading operation outside its boundaries, symbolic variable found")
                expr = z3.BitVec("mem_%s" %(var_mem_counter), size), []
                var_mem_counter += 1
            else:
                var = z3.BitVec("%s_addr_%s" %(dst, addr_mem_counter), self.__bits)
                addr_mem_counter += 1
                for addr in p_k:
                    cnc = z3.Concat(*[self.__mem[addr + i] for i in range( 0, size_b)])
                    expr = z3.simplify(z3.Or(var == cnc, expr))
                ret = expr, []
        else:
            addr = random.choice(self.__mem.keys())
            cnc = z3.Concat(*[ self.__mem[addr + i] for i in range( 0, size_b)])
            cnc = z3.simplify(cnc)
            ret = cnc, [dst == addr]

        return ret

    def get_bit_address(self):
        return self.__bits

    #TODO: copy-on-write behaviour
    def copy(self):
        return copy.copy(self)
{'fraction_non_alphanumeric': 0.13236549957301452, 'fraction_numerical': 0.015981456630474563, 'mean_word_length': 1.6565132858068696, 'pattern_counts': {'":': 0, '<': 13, '<?xml version=': 0, '>': 10, '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': '3577537', 'n_tokens_mistral': 2795, 'n_tokens_neox': 2644, 'n_words': 681}