Cleaner contracts

[SolalPirelli]

@tharvik this is a quick example of what I meant in our discussion yesterday as what index_pool's contract could look like instead of the current angr-dependent mess:

from klint import assume, any_bool, any_int, Map, sizeof
from klint.types import size_t, time_t, TIME_MAX, SIZE_MAX

# ideally we'd be able to use "not", "and", "or" but that requires patching the Python interpreter so... probably not
# instead, ~, &, | it is...

# I wonder if those doc comments are even needed? perhaps only optionally for the names of the function
# if they don't follow some convention (like struct_name_method_name), the parameters can probably be inferred?

class IndexPool:
    def __init__(self, size, expiration_time):
        """struct index_pool* index_pool_alloc(size_t size, time_t expiration_time)"""
        assert(size * sizeof(time_t) <= SIZE_MAX)
        self.size = size
        self.expiration_time = expiration_time
        self.items = Map(size_t, time_t)

    def borrow(self, time):
        """bool index_pool_borrow(struct index_pool* pool, time_t time, size_t* out_index, bool* out_used)"""
        assert(time != TIME_MAX)
        result = any_bool()
        index = any_int()
        used = any_bool()
        if self.items.length() == self.size:
            if self.items.forall(lambda k, v: time < self.expiration_time | (time - self.expiration_time) <= v):
                assume(~result)
            else:
                assume(result)
                assume(used)
        else:
             assume(result)
        if result:
            assume(index < self.size)
            if used:
                assume(self.items.contains(index))
                assume(time >= self.expiration_time)
                assume((time - self.expiration_time) > self.items.get(index))
            else:
                assume(~self.items.contains(index))
            self.items.set(index, time)
        return (result, index, used)

    def refresh(self, time, index):
        """void index_pool_refresh(struct index_pool* pool, time_t time, size_t index)"""
        assert(time != TIME_MAX)
        assert(index < self.size)
        self.items.set(index, time)

    def used(self, time, index):
        """"bool index_pool_used(struct index_pool* pool, time_t time, size_t index)"""
        value = self.items.get(index)
        if value is None:
            return False
        else:
            return time < self.expiration_time | (time - self.expiration_time) <= value

    def return(self, index):
        """void index_pool_return(struct index_pool* pool, size_t index)"""
        assert(index < self.size)
        self.items.remove(index)

Obviously just an example, I'm not even 100% sure it has all of the info necessary and only that, but I thought it'd be useful to write a clean version since the angr-specific one is a bit of a pain to understand.