diff --git a/greed/memory/lambda_memory.py b/greed/memory/lambda_memory.py index aa9cbcd..2883e51 100644 --- a/greed/memory/lambda_memory.py +++ b/greed/memory/lambda_memory.py @@ -274,15 +274,23 @@ def readn(self, index, n): self.add_constraint(Equal(res, BV_Concat(vv))) # print(f"actual readn {bv_unsigned_value(index)}:{n_val} = {BV_Concat(vv)}") return res - + def writen(self, index, v, n): + """Writes n bytes of a value (v) at a offset in memory (index). + + Args: + index: A YicesTermBV representing the offset in memory to write to. + v: A YicesTermBV representing the value to write to memory. + n: A YicesTermBVV representing the number of bytes to write to in memory. + """ assert is_concrete(n), "writen with symbolic length not implemented" assert bv_unsigned_value(n) != 0, "invalid writen with length=0" + n_val = bv_unsigned_value(n) self.invalidate_cache(start=index, end=BV_Add(index, n)) - for i in range(bv_unsigned_value(n)): - m = BV_Extract((31 - i) * 8, (31 - i) * 8 + 7, v) + for i in range(n_val): + m = BV_Extract((n_val - 1 - i) * 8, (n_val - 1 - i) * 8 + 7, v) self[BV_Add(index, BVV(i, 256))] = m # update cache