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.

Sign up for GitHub

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

Jump to bottom

Fix constant folding & constraint set slicing #1706

Merged
merged 57 commits into from
Jun 17, 2020
Merged

Fix constant folding & constraint set slicing #1706

Show file tree
Hide file tree
Changes from 3 commits
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
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -146,7 +146,7 @@ def __get_related(self, related_to=None):
break

variables = get_variables(constraint)
if related_variables & variables:
if related_variables & variables or not variables:
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

With this added "this" test passes with both get_related enabled and disabled

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As long as both are passing, let's set the default back to True

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well I'm not 100% This single testcase representes all possible fails explained in issue #1679

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Devils advocate, here... What if related_to is A and constraint is something like B && !B, i.e., constraint is unsatisfiable and has variables, but they do not overlap with those of related_to?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes get_related should work only on previously feasible path contraints.
If you have feasible A & B & C and want to check if B \/ C can be True then you do not need to bother the solver with the A.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes. I know it is not enforced.
We should make it a pre-condition or attempt to solve the full constraint set and trust that some cache magic prevents it to do the solving over the whole thing again and again.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes. I know it is not enforced.
We should make it a pre-condition or attempt to solve the full constraint set and trust that some cache magic prevents it to do the solving over the whole thing again and again.

I don't know how reasonable this approach is. __get_related is called by to_string, and to_string is something that one might reasonably call to debug a bad constraint set.

Moreover, to_string is called by can_be_true:

manticore/manticore/core/smtlib/solver.py

Line 433 in 2c90ee0

self._reset(constraints.to_string())

So there's a little bit of a chicken-and-egg problem here.

If it were up to me, I would not insist that __get_related be called on only satisfiable constraint sets.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Many constraints do not overlap in terms of the memory they reference. Constraint independence divides constraint sets into disjoint independent subsets based on the symbolic variables and memory cells they reference. By explicitly tracking these subsets, it can frequently eliminate irrelevant constraints prior to sending it to the solver.
For example, given the constraint set {i < j, j < 20, k > 0}, a query of whether i = 20 just requires the first two constraints. This was first explained in [EXE] https://web.stanford.edu/~engler/exe-ccs-06.pdf

We can move the optimizations/transformations that are controlled via kwargs in the to_string() to a different ConstraintSet method. Like slice_related_to(..) and make_bindings so it is done more explicit.

If the problem is to print a ConstraintSet for debugging you can just just do not slice the ConstraintSet.

print (str(cs))

There is also a forgotten pretty_print for expressions.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fwiw, I use the pretty_print all the time while debugging

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Moved the disabled get_related as a special method of a ConstraintSet to slice it when the user wants it.
Also added "some" tests for it.

remaining_constraints.remove(constraint)
related_constraints.add(constraint)
related_variables |= variables
Expand Down
Binary file added tests/ethereum/data/ErrRelated.pkl.gz
View file
Open in desktop
Binary file not shown.
34 changes: 34 additions & 0 deletions tests/ethereum/test_regressions.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -353,6 +353,40 @@ def test_mulmod(self):
# 0x8000000000000000000000000000000000000000000000000000000082000011
self.assertEqual(Z3Solver.instance().get_all_values(constraints, result), [2423129])

def test_related_to(self):
import gzip
from manticore import config
from manticore.core.smtlib.visitors import translate_to_smtlib
from manticore.core.smtlib import ConstraintSet, Z3Solver, Operators, BitVecConstant
import pickle, sys
filename = os.path.abspath(os.path.join(DIRPATH, "data", "ErrRelated.pkl.gz"))
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What's in this file?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Also, should this test be in ethereum directory?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

My guess is that it's a state that exhibits the get_related bug, but pickled and gzipped so that we don't need to construct it from the source code.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes. Not the state but the ConstraintSet that showed the problem. This is not really ethereum specific.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is it expensive to construct from source? A binary isn't easy to peruse over the web, for example.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I saved the constraint and the constraintset that found to have trouble with old get_related.
I re build the constraint but the constraintset was big ish so I left it all binary and obscure.
Its a hack. I'll be much better to produce the testcases ourselves.
As it is still disabled by default I could remove this unintelligible test.


constraints, constraint = pickle.loads(gzip.open(filename,'rb').read())

consts = config.get_group("smt")
feliam marked this conversation as resolved.
Show resolved Hide resolved
consts.related_constraints = False

Z3Solver.instance().can_be_true.cache_clear()
ground_truth = Z3Solver.instance().can_be_true(constraints, constraint)
self.assertEqual(ground_truth, False)

consts.related_constraints = True
Z3Solver.instance().can_be_true.cache_clear()
self.assertEqual(ground_truth, Z3Solver.instance().can_be_true(constraints, constraint))

#Replace
new_constraint = Operators.UGE( Operators.SEXTEND(BitVecConstant(256,0x1a),256,512) * BitVecConstant(512,1), 0x00000000000000000000000000000000000000000000000000000000000000010000000000000000000000000000000000000000000000000000000000000000 )
self.assertEqual(translate_to_smtlib(constraint), translate_to_smtlib(new_constraint))

consts.related_constraints = False
Z3Solver.instance().can_be_true.cache_clear()
self.assertEqual(ground_truth, Z3Solver.instance().can_be_true(constraints, new_constraint))

consts.related_constraints = True
Z3Solver.instance().can_be_true.cache_clear()
self.assertEqual(ground_truth, Z3Solver.instance().can_be_true(constraints, new_constraint))



if __name__ == "__main__":
unittest.main()