Symbolic memory model bugfixes #1350
Conversation
manticore/core/smtlib/expression.py
Outdated
| @@ -308,6 +308,10 @@ def __ror__(self, other): | |||
| def __invert__(self): | |||
| return BitVecXor(self, self.cast(self.mask)) | |||
|
|
|||
| def __len__(self): | |||
| """Returns the bitvector size, in bytes(!)""" | |||
| return self.size // 8 | |||
There was a problem hiding this comment.
@feliam is it fine to return the length of a BitVec in bytes?
There was a problem hiding this comment.
idk. It is a bit vector.
pyZ3 does not use len but rather a bv.size()
We should carefully check that it is not used for bits anywhere.
There was a problem hiding this comment.
@ehennenfent any context why do we need to add this in the first place?
There was a problem hiding this comment.
Pretty sure the original reason was to allow this assert to pass when using a memory model that returns a BitVec.
There was a problem hiding this comment.
We need a way to read the size of a bitvec. Maybe using _len is not the best way.
We already have .size
Are we sure we'll never support a 4 bit bitvec?
It may be better if we remove it (__len__).
There was a problem hiding this comment.
We've since found a way to make the symbolic memory model work without this workaround, so if you think it's better to delete than risk setting ourselves up for failure later, that's fine with me.
| @@ -583,7 +583,7 @@ def _update_cache(self, name, value): | |||
| self._cache.pop(affected, None) | |||
|
|
|||
| def read(self, name): | |||
| name = self._alias(name) | |||
| name = str(self._alias(name)) | |||
There was a problem hiding this comment.
For context, this prevents an issue on line 591, where Python doesn't like evaluating if 'FLAGS' in name: if name is not a string. I don't remember how I triggered it, but since the name should already be a string in most reasonable cases, I don't think this will break any functionality.
* master: Ensure native deps (better error message) (#1367) Make sys_lseek return offset location (#1355) Fix a typo in the documentation (#1360) Refactor tests structure (#1352) Dev single gas calc (#1353) Symbolic memory model bugfixes (#1350) Refactor not-existing SValue into BitVecVariable Config with context (#1345) Update Capstone to 4.0.1 (#1312) evm: fix _check_jumpdest when run with detectors (#1347) Move tx default gas value to config (#1346)
Handles edge cases that sometimes occur with symbolic memory models. Nothing major, just merging so we can delete the branch.
This change is