Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix constant folding & constraint set slicing #1706

Merged
merged 57 commits into from
Jun 17, 2020
Merged
Changes from 1 commit
Commits
Show all changes
57 commits
Select commit Hold shift + click to select a range
0cd1bc5
Add ONE failing test
feliam May 13, 2020
609a37e
Fix test
feliam May 13, 2020
b29f3ac
Try fix get-related
feliam May 13, 2020
79aa5cc
Move regression to other
feliam Jun 2, 2020
7339eb9
blkn
feliam Jun 2, 2020
c121c38
blkn
feliam Jun 2, 2020
3ff6b95
Move get related
feliam Jun 5, 2020
02b4c69
Merge branch 'master' into dev-get-related
feliam Jun 5, 2020
00e8199
CC
feliam Jun 5, 2020
6b7f671
fix concolic
feliam Jun 5, 2020
6732eb2
lint
feliam Jun 5, 2020
4adeac2
DivByZero default to zero
feliam Jun 5, 2020
7565b4a
blkn
feliam Jun 5, 2020
1680397
Update manticore/core/smtlib/solver.py
feliam Jun 5, 2020
cbe55b9
Update manticore/core/smtlib/constraints.py
feliam Jun 5, 2020
315ef64
Update manticore/core/smtlib/constraints.py
feliam Jun 5, 2020
6155a4d
remove odd string
feliam Jun 5, 2020
38dbfd6
Merge branch 'dev-get-related' of github.com:trailofbits/manticore in…
feliam Jun 5, 2020
1491cbd
lint
feliam Jun 5, 2020
264eb04
mypy lint
feliam Jun 5, 2020
e0130a4
Update manticore/core/smtlib/visitors.py
feliam Jun 5, 2020
d0e9abf
lint
feliam Jun 5, 2020
9807b37
Add Docs
feliam Jun 8, 2020
728e021
Merge branch 'master' into dev-get-related
feliam Jun 9, 2020
e584fb2
merge
feliam Jun 9, 2020
bf3a2b9
Replace modulo with masks
Jun 10, 2020
3eb96f8
Blacken
Jun 10, 2020
5e54189
blkn
feliam Jun 10, 2020
a0ab429
Merge branch 'dev-get-related' of github.com:trailofbits/manticore in…
feliam Jun 10, 2020
536ec71
fix mypy
feliam Jun 10, 2020
a83e8c2
fix mypy
feliam Jun 10, 2020
37144d9
Add tests for signed LT behavior
Jun 10, 2020
1b8754d
New test
feliam Jun 10, 2020
787e51f
Fix constant folding
feliam Jun 10, 2020
dca9adb
merge
feliam Jun 10, 2020
dfa7a84
lint
feliam Jun 10, 2020
b841038
lint
feliam Jun 10, 2020
735a963
lint
feliam Jun 10, 2020
b54a448
Unittesting power
feliam Jun 10, 2020
02563cd
Permisive read_buffer
feliam Jun 10, 2020
3fab981
Preserve precision in constant folding
Jun 10, 2020
f7fb8bb
Strip left-in print debugging
Jun 11, 2020
2f5d4d2
fix wasm
feliam Jun 11, 2020
18064f8
Merge branch 'dev-get-related' of github.com:trailofbits/manticore in…
feliam Jun 11, 2020
52d8eb4
Fix
feliam Jun 11, 2020
f1dfb80
REmove get_related from the default path and fix arm test
feliam Jun 12, 2020
d5b577e
blkn
feliam Jun 12, 2020
79b42ed
fix related to tests
feliam Jun 12, 2020
ec8489f
blkn
feliam Jun 12, 2020
2113a73
Fix bug in test and disable debug messages in Solver
feliam Jun 12, 2020
c2a21ba
smtlib config to disable multiple check-sat in newer z3
feliam Jun 12, 2020
f87e1e2
Disable log test and fix merging poc vs variable migration
feliam Jun 15, 2020
2eb630d
blkn
feliam Jun 15, 2020
8818ea3
Avoid exception in some callbacks
feliam Jun 15, 2020
27db1b8
can_raise at did_will
feliam Jun 15, 2020
64a03a7
slightly better z3 onfiguration
feliam Jun 16, 2020
380fb31
lint
feliam Jun 16, 2020
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion manticore/core/smtlib/constraints.py
Original file line number Diff line number Diff line change
Expand Up @@ -116,7 +116,7 @@ def _get_sid(self) -> int:
self._sid += 1
return self._sid

def related_to(self, related_to: Optional[Expression] = None):
def related_to(self, related_to: Optional[Expression] = None) -> ConstraintSet:
feliam marked this conversation as resolved.
Show resolved Hide resolved
# sam.moelius: 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
Expand Down