* Add Manticore native State-specific hooks
* Add tests
* Add type hints when setting state
* Add back needed assertion for PC hook
* Test that hook actually executes in test
Co-authored-by: Eric Hennenfent <[email protected]>
* Linux: Add stat method for FdLike
* Add tests
* Don't try to cover abstract class function bodies
* Update test file names
* Try again to not cover abstract methods
* Add typehint to Directory stat()
Co-authored-by: Eric Hennenfent <[email protected]>
* Fix typehints with os.stat
* Adjust type for stat object
Co-authored-by: Eric Hennenfent <[email protected]>
* Use default handler for symbolic system call arguments
This will only be called when there is an implementation of the system
call in the concrete Linux class and no implementation in the symbolic
SLinux.
The action is simply to concretize any found symbolic system call
arguments.
This should hopefully ease the use of Manticore when it encounters
symbolic arguments to system calls that don't have specially implemented
symbolic handling. A debug message is printed when this happens.
* Make sure to return passed implementation
* Use rsplit instead of indexing to get owner class of method
Co-authored-by: Eric Hennenfent <[email protected]>
* Use coveralls
* Use python coveralls
* Try again with different casing
* Use coveralls repo token from web page
* Use GITHUB_TOKEN in github action parallel-finished
* Remove codecov config
* Add note for final coverage job
* Swap Readme coverage badge
* Add strncpy model
* Forgot to remove an edit
* Adding model tests
* Added strncpy c file and created a directory for all string modeling binaries
* Update to argument ordering in manticore/native/models.py
Co-authored-by: Eric Kilmer <[email protected]>
* Removed dead code
Co-authored-by: Eric Kilmer <[email protected]>
* New working model of strlen - Symbolic Test yet to be updated
* Updated modeling test for all symbolic input
* Fixed code climate issue
* Adding binary for new test
* Updated test to use sets for compairison
* Removed length compairison
* Fix argument concretization indexing
* Preserve both model implementation strategies
* Corrected formatting
* Removed whitespace for code climate
* Removed whitespace for code climate
Co-authored-by: Eric Kilmer <[email protected]>
* Revert 1e23f7ab
Remove psutil as a dependency
* Bump version numb, update changelog
* Re-do updated model not available message
* Update for latest PRs
* Update dates
* Add ONE failing test
* Fix test
* Try fix get-related
* Snapshots
* CC
* Allow snapshooting just from main()
* A test
* Test and fix is_main
* CC
* review
* ismain vs is_running
* is main to is main script
* Remove unused member variable
* initial import manticore verifier
* Fix verifier installation
* clear ready states
* CC and smoke test
* CC
* Increase cov
* Move regression to other
* blkn
* blkn
* Move get related
* CC
* fix concolic
* lint
* DivByZero default to zero
* blkn
* Update manticore/core/smtlib/solver.py
Co-authored-by: Eric Kilmer <[email protected]>
* Update manticore/core/smtlib/constraints.py
Co-authored-by: Eric Kilmer <[email protected]>
* Update manticore/core/smtlib/constraints.py
Co-authored-by: Eric Kilmer <[email protected]>
* remove odd string
* lint
* mypy lint
* Update manticore/core/smtlib/visitors.py
Co-authored-by: Eric Kilmer <[email protected]>
* lint
* Add Docs
* blkn
* blkn
* Replace modulo with masks
* Blacken
* blkn
* fix mypy
* fix mypy
* Add tests for signed LT behavior
* New test
* Fix constant folding
* lint
* blkn
* lint
* Fixes...
* lint
* Unittesting power
* Permisive read_buffer
* Fix optimize
* Preserve precision in constant folding
* Strip left-in print debugging
* blkn
* remove wasm_sym temporarily
* Better simplification for constants
* Add json
* blkn
* Better commmandline args
* blkn
* fix wasm
* Fix
* better commanlining
* REmove get_related from the default path and fix arm test
* blkn
* fix related to tests
* blkn
* Fix bug in test and disable debug messages in Solver
* smtlib config to disable multiple check-sat in newer z3
* Disable log test and fix merging poc vs variable migration
* blkn
* Avoid exception in some callbacks
* can_rais at did_will
* yikes!
* blkn
* Yices found one more states in truffle
* Add a config constant to ignore symbolic balances
* Add a config constant to ignore symbolic balances 2
* Relax truffle state count
* Relax truffle state count 2
* Change cli name and test
* Clear redy states in verifier workspace
* Clear ready states in verifier workspace
* Relative ws path on verifier output. Clean CREATE testcase example
* Blkn
* Improve coverage and funcid solving
* lint
* Better testcase generation at verifier
* Better testcase generation at verifier and typos
* Better output and default re
* Test must revert
* Better output and default re
* move generate_testcase_ex to private method
Co-authored-by: Eric Kilmer <[email protected]>
Co-authored-by: Eric Hennenfent <[email protected]>
* Experiment with testing on OSX
Not committing to front-lining OSX support as a feature because there are some fundamental performance concerns, but I would like to see how the tests behave.
* solc --> usr/local/bin
* Don't fail fast
* Require Unicorn 1.0.2rc2
¯\_(ツ)_/¯
* Update Bash on OSX builds
* Use mac solc
* Simpler solidity installation
* Fix wasm tests maybe?
* Swap `ls` args in truffle tests
* Good 'ol printf debugging
* OSX Keystone install
* Truffle test miscounting fix?
* Add unzipping timeout
* Remive timeout _and_ `yes`
* Allow output check to work on OSX
* Add list wrapper to filter
* Remove print statements
* yolo keystone via homebrew
* Try again w/ Keystone Brew
* typo
* Create osx.yml
* Revert to Master's ci.yml
* Update to checkout@v2 universally
* Save checkout version change for another PR
It maybe breaks codecov?
* Add Truffle Tests
* Fix Truffle
* Make native an option
* See if native works?
* Revert "See if native works?"
This reverts commit ce90d8bcb0.
* Replace actions content w/ script
* Update number of Truffle tests
* Force working directory
* Remove shebang, fix YAML
* Fix incorrect path to script?
* Why are the docs always wrong
* YAML syntax
* Fix usage of GITHUB_WORKSPACE
* Forget the workspace, just copy the script to the root
* Revert workspace path changes
* Fix VM test generation
* Whitespace fixes
* Only run on a schedule
* Install Yices and CVC4
* Working copy for strcpy - without symbolic input
* Corrected null term error
* Needs to be tested but general algorithm idea for handling symbolic input
* Updated according to feedback
* Beginning of strcpy tests
* Revising strcpy algorithm - realised it was flawed
* This should be a more correct way of handling symbolic bytes. Needs testing
* Get rid of redundant code
* Fixed another typo
* Update manticore/native/models.py
Co-Authored-By: Eric Kilmer <[email protected]>
* Clarified and updated comments
* Fixed some errors in model while working on tests
* Progress on tests
* Found typo in models
* Removed unnecassary whitespace
* Added some helper functions for tests and to clean things up
* Added comments for helper functions
* WIP: current state of strcpy tests
* Updated type hints from Expression to BitVec
* Fixed linter complaints
* Updated strcpy return type to make linter happy
* Added some helper properties to expression BitVecITE
* Overwrote equal op in ArraySelect
* Fixed formatting in expression
* Almost done just needs some cleaning
* Attempt at overriding __eq__ again
* Cleaned up tests some still have unresolved __eq__ issues
* Removed stuff from expression and updated test_models.py
* Removed stuff from expression and updated test_models.py
* Basicly done probably needs some more comments for clarity
* Cleaned up the tests a little
* Corrected linter error and added more comments to strcpy model functions
* Remove duplicated word in comment
Co-authored-by: Eric Kilmer <[email protected]>
* Update manticore/native/models.py
Co-authored-by: Brad Larsen <[email protected]>
* Update manticore/native/models.py
Co-authored-by: Brad Larsen <[email protected]>
* Update tests/native/test_models.py
Co-authored-by: Brad Larsen <[email protected]>
* Updates according to feedback
* Swapped can_be_true and must be true
* Updates for feedback
* Forgot to lint
* Fixed some typos
* Largely simplified ITE being built
* Forgot to lint
* This is messy but seems to be concretizing to the correct states
* Very very messy state of the code before attempting to concretize on every possible NULL
* Cleaned up model with forking on every possible NULL
* Removed trailing whitespace for CodeClimate
* Added state.context for offset value back
* New symbolic test with regex for expected output
* New symbolic test with regex for expected output
* Updated for mypy
* Updated comments in tests
* Updated cant_be_null to cannot_be_null
* Corrected docstring location for _test_strcpy
* Add break for efficiency
* Added compiler information and source file
* Updated regex to use raw strings
Co-authored-by: Eric Kilmer <[email protected]>
Co-authored-by: Brad Larsen <[email protected]>
* Snapshots
* CC
* Allow snapshooting just from main()
* A test
* Test and fix is_main
* CC
* review
* ismain vs is_running
* is main to is main script
* Remove unused member variable
* Fix is main variable
* Update manticore/core/manticore.py
Co-authored-by: Eric Hennenfent <[email protected]>
* review
* blkn
* Betteer Exception handling
* Lint and test
Co-authored-by: Eric Hennenfent <[email protected]>
* Use merge SHA instead of head
Github Actions doesn't update the head variable despite the checkout action merging the active branch into `master`, so the commit range specified was invalid
* Start from common ancestor
* Omit explicit SHA
* Lint HEAD instead of merge
* Manually fetch base SHA
* Print the names of files to be diffed
* Update ci.yml
* Modify a Python file
* Blacken everything that was missing
The modified files got missed due to black not properly running on our CI
* Experimental coverage changes
Tells coverage.py to record coverage for individual test cases, and makes CodeCov tolerate a small drop in overall coverage percentage to account for nondeterministic gas tests.
* Use workspace
* Remove explicit concurrency type declaration
Appears to break use of subprocess in integration tests
* Eliminate dynamic context
* Make all CI respect rcfile
* Use environment variable
* Rewind cpu when ConcretizeArgument is raised in system call
* Remove unused ConcretizeSyscallArgument
* Add test for symbolic system call argument
* Roll back PC during handling of ConcretizeArgument
This accomplishes the same thing as before but now the movement is done
in the parent state instead of children states
* Statically link test executable
* Use simple checkpoint and rollback for PC
* Rework checkpoint and rollback in exception-handling
* Create rollback function in State
This is to make sure we don't miss anything when adding future values
* Define only one local variable for exception data
* Remove unused import
* Less verbosity in test
* Rollback in parent state instead of children states
* Always rollback state on Concretize*
* Use typing.NamedTuple
Thank you @bradlarsen
* Use local checkpoint variable
We don't access checkpoint data anywhere else aside from the `execute`
function
* Add type hint to test
Co-authored-by: Brad Larsen <[email protected]>
* Use more specific language in test comment
Co-authored-by: Brad Larsen <[email protected]>
* Remove outdated function name in comment
* Fix missed refactor
* Remove unneeded testing changes after refactor
Co-authored-by: Brad Larsen <[email protected]>
* Fix inheritance magic nonsens and add plugin enable/disable
* CC
* Better Plugin default
* Fix enabled default
* Trying to generalize enable/disable for plugins
* Merger is the only plugin using locked context correctly
* Fix plugin context name
* text to enum
Overhaul Linux file emulation.
Previously, open file descriptors could be mapped to any of the `File`, `Directory`, `SocketDesc`, `Socket`, and `ProcSelfMaps` classes, which didn't share a common supertype, and which didn't have consistent interfaces.
Now, each of these classes implements the `FdLike` abstract base class, which specifies a number of methods.
This overhaul additionally fixes several issues with the Linux support code:
- A program that tried to ioctl on a socket would crash Manticore
- In several places, the error code returned by a failing syscall was incorrect
- Many file descriptor operations could crash Manticore when used on an already-closed descriptor
- Manticore state serialization / deserialization was incorrect for file descriptor types other than File or Socket
- In certain cases, `sys_open` / `sys_openat` could crash Manticore when trying to log a debug message
- In certain cases, `sys_readv` could crash Manticore, instead of correctly returning a negative int value
- `sys_sendfile` was broken due to a variable name typo
- In several places in Manticore’s Linux support code, incorrect type hints were present
- In some places, an exception would attempt to be raised, but that itself would crash due to a missing import.
This commit adds two more example / integration test programs.
Additionally, this adds a helper for working with Python abstract base classes. This helper lets you declare on a class, via a decorator, that the class is expected to have no unimplemented abstract methods. If this is not true at runtime, a `TypeError` is thrown. Without this decorator, you will only discover that a class has unimplemented abstract methods when you try to _instantiate_ that class. This may be much, much later than at class creation time, or perhaps not at all, depending on your code coverage.
Thanks to Eric Kilmer <[email protected]> for review!
feliam