* Fix a few documentation typos in ManticoreBase
* Fix documentation in ManticoreBase: 'vervosity' -> 'verbosity'
Co-authored-by: Eric Hennenfent <[email protected]>
There is a flaw in how __get_related works: when called on certain
unsatisfiable sets, it can return a satisfiable one. The flaw arises when:
* self consists of a single constraint C
* C is the value of the related_to parameter
* C contains no variables
* C is unsatisfiable
Since C contains no variables, it is not considered "related to" itself and is thrown out
by __get_related. Since C was the sole element of self, __get_related returns the empty
set. Thus, __get_related was called on an unsatisfiable set, {C}, but it returned a
satisfiable one, {}.
* Make CodeCov wait for reports from all CI jobs
This should prevent the red 'X' from appearing as soon as the first job finishes.
* Make CI step fail if codecov fails to upload
* Run examples with coverage
* Copy coverage file appropriately
* Fix path to coverage file
* Add comment about n builds
* Disable failing CI upon error.
* Rework syscall invocation for proper behavior under typeguard
Previously, using Typeguard with Manticore would break several emulated
syscalls. With this commit, it does not.
Some background information:
When a syscall is made from an emulated binary, Manticore uses the
syscall number to look up the appropriate Python method that models that
syscall, and then uses Python introspection to massage arguments to that
syscall model function as deemed appropriate.
Previously, this mechanism used the deprecated `inspect.getfullargspec`
to determine the number of arguments to the model function, and whether
or not it takes varargs.
However, `inspect.getfullargspec` doesn't look through wrapper
functions; it looks only at exactly the function object it is given.
This is an issue, however, when trying to inspect _decorated_ functions.
(The use of a decorator in Python introduces a _new_ function object
that wraps the decorated item.)
How did that break Manticore when using Typeguard? It turns out that
When using Typeguard via the `--typeguard-packages=manticore` option to
`pytest`, the Typeguard plugin implicitly adds a `@typeguard.check_types`
decorator on _every_ function & method in the `manticore` package.
In this way, each syscall implementation function in Manticore ends up
with a wrapper around it, and the syscall invocation mechanism based on
`inspect.getfullargspec` would somewhat quietly cause syscalls to break.
Now, instead of using `inspect.getfullargspec`, Manticore's syscall
invocation mechansim uses the non-deprecated `inspect.signature` API to
get the needed information. This API _does_ look through wrapper
functions. Additionally, it allows us to get rid of some conditional
logic, about whether `self` appears in a function's parameter list or
not.
* Update manticore/native/cpu/abstractcpu.py
* Get rid of the `wrapt` library
We only were using `wrapt` in a single place -- to implement the
`unimplemented` syscall decorator. That dependency was added in #1384,
so that the old syscall mechanism could work with the decorator.
Now, with the rework of Manticore's syscall mechanism, this is no longer
necessary, and a "regular" Python decorator implemented using
`functools.wraps` should work just fine.
* Fix rewrite of `unimplemented`
* Rework platform `unimplemented` decorator, take 3
Additionally, add some extra tests for the decorator, to get better
coverage from where it is used.
* Clean up `test_sycalls.py` imports
* Fix an unbound variable error
(found with `mypy --check-untyped-defs` and some grep)
* Get rid of some unused imports
* Delete simultaneously dead & broken code
* Fix an overly specific type hint in smtlib `Bool.cast`
* Fix type confusion in Solver internal methods
* Fix type confusion in Linux symbolic file support
* Fix type confusion in Linux platform & abstract CPU
* Fix an incorrect type hint & clarify documentation in Linux `sys_open`
* Fix type confusion in `unimplemented` decorator
* Remove some `Generator` return type signatures; mypy/typeguard/`@contextmanager` do not agree with each other
* Delete a couple bad type hints
The `dirfd` and `buf` parameters can be symbolic, and the type-checking
that mypy does has trouble understanding `issymbolic`. So, un-type-hintify
those parameters.
* Add type hints & fix typing issues in manticore.core.workspace
* Remove some wrong type hints from AbstractCpu
It turns out that the type of `data` in a couple methods is pretty flexible,
and our tests use more than just `str`, `bytes`, and `List` types for that
parameter.
It is not quite clear what requirements there actually are on `data`, and so at
least for now, get rid of the type hint there.
* Add type hints & fix a typing issue in manticore.native.cpu.x86
**kwargs could not have possibly worked in `AMD64Operand`.
* Make the type hint of `Z3Solver._send` tighter.
* Update manticore/core/workspace.py
Remove unused import (thanks @ehennenfent!)
* Use more specific types (thanks @ehennenfent!)
* Add type hints
* Add type hints in manticore/core/smtlib/solver.py
* Add type hints to the `unsigned_hexlify` helper function
* Add type hints & more robust error checking to a Solver internal method
* Add type hints in native memory code
* Add type hints to Linux platform test methods
* Add type hints for Linux `sys_access`
* Add type hints for AbstractCPU; rephrase a couple bits to appease mypy
* Add type hints to manticore/platforms/linux.py
* Add type hints for Workspace members
* Add type hints for `Operand`
* Add a return type hint per @ekilmer
Co-Authored-By: Eric Kilmer <[email protected]>
* Remove unused arg ans separate output from workspace
* Update docstring on ManticoreBase
Fix missing docstring for outputspace_url
Co-authored-by: Eric Hennenfent <[email protected]>
* Add type hints to some Linux syscalls
* Fix a type error & add a type hint in Linux `sys_open`
* Add an example program that can exercise symbolic file support
* Add a test case based on the `fileio` example
Note, The `fileio_linux_amd64` test binary was manually copied from the
examples directory and added to Git. Maybe one day we will come up with
a more principled mechanism for this.
Also note, this test case currently fails, even with the `sys_open` type
fixes. Multiple errors are revealed by this test case.
* Add a type hint
* Add type hints to manticore workspace code
* Make an optional parameter non-optional
This function never seems to be used without specifying the formerly
optional value.
* Fix choice of abbreviation in comments
* Allow keys with `/` in them in `FilesystemStore`.
This is an expedient fix -- a more proper fix would nail down the API of
which characters are allowed in keys, maximum length etc, at the level
of the `Store` class.
* Have `fileio` exit with 0 on incorrect usage
Our GitHub CI has one step where it builds each of the example programs,
and then attempts to run them with no arguments and no standard input,
checking that they exit with code 0. Rather than rework this approach
to support more general invocation patterns for example programs, it's
easier to change the `fileio` example I added.
* Blacken manticore/core/workspace.py
* py/missing-call-to-init
* Remove deprecated should_profile argument
* WASM __init__ call and variable names
* Mute warnings about printing evm account IDs
LGTM thinks we're logging potentially sensitive data when we create a symbolic account and print the user ID. I can't imagine a context where we would ever care about this alert in general, so I'm going to disable it.
* Fix mixed attribute/function names
* Another missing __init__ call
* Remove single-op form of _bitwise_instruction
It's never used
* Use built-in ops instead of lambda
* Missing import
* Some unreachable code
Still missing some in evm.py
* Blacken
* Tag examples as examples
* NotImplemented -> NotImplementedError
* Fix unnecessary `pass`
* Revert "Remove single-op form of _bitwise_instruction"
This reverts commit 1b7a4110f4.
* Mute overzealous call argument error
Co-authored-by: Brad Larsen <[email protected]>
* Fix typos.
* Create StackItem type alias.
* New failing tests demonstrating Wasm branching bugs.
The issue is that the Wasm symbolic execution engine concretizes the
integer input to branching instructions. Aside frome being
inefficient, the concretization logic prevents forking into more than
a small number of values and silently skips exploration of other
values.
* Fix for wasm if and br_if execution.
The engine raises a ConcretizeCondition exception to determine the
branch path and constrain the state minimally.
* Remove unnecessary bitwise AND.
It's unnecessary because c_int32 truncates to 32 bits and it's weird
because this bitwise and isn't there for I64.
* Failing tests demonstrating bug in br_table and call_indirect.
* Fix bugs with br_table and call_indirect using concrete conditions.
* Fix typing errors.
* Try to get wasm tests passing.
* Move advice conditions from Stack to separate structure.
* Fix so that multiple conditions may be concretized.
* Update incorrect comment on StateBase.concretize.
* Appease type checker.
* Add feature for SymbolicSocket through sys_accept
SymbolicSocket will generate symbolic bytes and variables on-demand
through interaction with the relevant system calls
* Fix comma in comment
* Add test for sys_read of symbolic socket
* Add type hints for Socket
* Add type hints for a couple abstract CPU functions
* Make sys_open / sys_openat debug log messages more descriptive
* Fix & comment out dead load_vdso code
* Add type hints in Linux platform code
* Add type hints & fix Liskov-substitution-principle-violating `seek` method overrides
* Add several more type hints for native memory code
* Eliminate a couple misleading log messages
* Add type hints & fix several edge cases in Linux filesystem emulation
* Refine logger messages from Linux syscalls
* Simplify a bit of code & add a type hint that got lost earlier
* Delete dead VDSO code in the Linux platform
* Add type hints & fix issues in memory map objects
There has been an inconsistency in the `__init__` methods of the `Map`
superclass and its subclasses, specifically with regard to `**kwargs`.
Example: previously, in `Arraymap`, `**kwargs` would be taken but
silently ignored.
* Eliminate parameter types from docstrings when type hints have been used instead
Additionally, add some more type hints from looking at methods that
immediately `assert isinstance(SOME_PARAM, SOME_TYPE)`. (These ought to
be non-controversial types.)
* Make a type more precise, courtesy of @ekilmer
* Restore an accidentally-deleted type signature
* Fix broken type hints
`Eventful` is not yet defined at the point the hint is used,
so use a forward reference instead. Similar with the use of `Cpu`.
* Fix bungled type hint
* Blacken manticore/native/cpu/abstractcpu.py
* Restructure SMTLib to avoid multiple inheritance
* Attempt to fix usage of Constant/Variable/Operation outside of expressions
* Fix init arguments
* Fix missing return statement in visit_ArraySelect
* Add Missing ArrayVariable
* Extraneous return statement
* Rename ConstantType, VariableType, and OperationType
Remove the 'Type' to make the diff smaller
* Add __slots__ in Expressions
* Blacken...
* Fix mypy
* Fix dropped array operand
* Return output from visit_operation properly
* Shrink diff
* Shrink Diff 2
* Clean up visitor rewrite
Much smaller diff now
* Maybe this will fix the truffle tests?
Who knows...
* Remove NVM
* Use setdefault for taint
* Add test to check for required properties
It turns out that in smaller programs, like
examples/linux/binaries/multiple-styles, something like 15-20% of total
runtime is spent redundantly initializing the Z3 solver!
* Add an implementation of sys_llseek for Linux
* Reformat a couple funny string literals
* Add a docstring for `sys_llseek`
This was taken mainly from the manpage.
* Fix a broken log format string
* Improve logging & exception messages in linux platform
* Update docstring for sys_lseek
* Remove redundant space in mmap mode strings
* Clean up temp files after linux platform tests
* Add some tests for the `sys_lseek`
* blacken tests/native/test_syscalls.py
* Fix implementation of sys_llseek; expand & refine tests
* blacken manticore/platforms/linux.py
* Add some type signatures
* Fix type signatures; add more signatures
* Fix a bad variable reference
* More type signatures; fix typing issues with linux `sys_write()`
* Added support for proc/self/maps
* Corrected formatting
* Updated ProcSelfMaps object
* Fix for codeclimate
* Updates according to Eric H.'s feedback
* Added a data class for ProcSelfMapInfo. May make a few more adustments to this
* Changed address to a property in ProcSelfMapInfo
* adding a rust binary test
* Added a test for proc self to test_linux
* Updated the address and perms property tests to use a regex
* Updated the regex check
* `PickleSerializer`: transparently use gzip
* Move an import to the module top-level
* Rename `manticore.core.workspace.Testcase` class to avoid pytest collection warning
* Fix a deprecation warning in workspace test code
* Use a lower compression level on serialized states
The default for Python's GzipFile is `9`, the highest possible
compression level. This is analagous to the compression level option
for the `gzip` command-line program.
I ran some experiments, and with the default compression level of 9,
serialized state files end up _much_ smaller. However, Manticore ends
up running measurably slower. With this change to set the compression
level to `5`, the serialized state files are still much smaller (~13x
smaller than uncompressed), and Manticore runs _faster_ than without any
compression of state files.
* Add a comment & parameterize a magic number
* Use `.pkl.gz` for compressed pickle state file extension
* Decrease compression level to gzip minimum
This maybe makes things run faster, but also does not seem to decrease
the compression ratio seen for state pickle files.
* Revert "Use `.pkl.gz` for compressed pickle state file extension"
This reverts commit c148e61f9f.
* Add config variable to disable compression
* Fix missing decompression parameter
Co-authored-by: Eric Hennenfent <[email protected]>
Samuel Moelius