@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.
@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: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.