TLDR: This is not helpful when looking at `lint` build output:
```
$ black --check manticore/core/smtlib/solver.py
would reformat manticore/core/smtlib/solver.py
Oh no! 💥💔💥
1 file would be reformatted.
```
And this is more helpful:
```
$ black --diff --check manticore/core/smtlib/solver.py
--- manticore/core/smtlib/solver.py 2019-11-24 11:14:37.431508 +0000
+++ manticore/core/smtlib/solver.py 2019-11-24 12:09:00.461367 +0000
@@ -149,13 +149,11 @@
self._proc: Popen = None
# z3 parameters can be listed via `z3 -p` and set on the CLI
parameters = "parallel.enable=true"
- self._command = (
- f"{consts.z3_bin} -t:{consts.timeout*1000} -memory:{consts.memory} -smt2 {parameters} -in"
- )
+ self._command = f"{consts.z3_bin} -t:{consts.timeout*1000} -memory:{consts.memory} -smt2 {parameters} -in"
# Commands used to initialize z3
self._init = [
# http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_AUFBV
# Closed quantifier-free formulas over the theory of bitvectors and bitvector arrays extended with
would reformat manticore/core/smtlib/solver.py
Oh no! 💥💔💥
1 file would be reformatted.
```
* Little test refactor/improvement
* SMemory.write refactor
* Optimize concrete writes of multiple bytes to memory
* Fix record writes tests
* Blackify
* Blacken
* Fixes ConstraintSet.new_bitvec size check
Previously the `new_bitvec` checked for `size == 1 or size % 8 == 0`.
This check allowed to create a bitvec with negative size, as in `cs.new_bitvec(-8)`.
It was also too constrained, as we might have cases where we want to constraint ourselves to e.g. 5 bits out of 8 bits of a byte). Sure, this can be done via setting a constrain over an 8-bit (1 Byte) bitvector, but it might be not the most efficient solution(?).
* Add testcase for invalid cs.new_bitvec size
* Fix operators.ORD for BitVecs of size > 8
TLDR: `ORD(s)` should return something that has 8 bits instead of 7, which it incorrectly did for BitVecs with size>8.
Note that the `ORD` still does not support `BitVec`s with size<8, but I am not sure if we need that support for now. To be clear, such situation ends up as an assertion failure that is being done in `BitVecExtract`, so when assertions are gone (for optimized launches) we might want to extend `ORD` to support it.
* Add proper ORD fix testcase
Disconnect3d