* 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!
* 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.
Sonya Schriner