smt: abstract multiplication #340
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
0xkarmacoma
reviewed
Aug 13, 2024
src/halmos/sevm.py
Outdated
| return w2 | ||
|
|
||
| if is_power_of_two(i1): | ||
| return w2 << int(math.log(i1, 2)) |
There was a problem hiding this comment.
Suggested change
| return w2 << int(math.log(i1, 2)) | |
| return w2 << i1.bit_length() - 1 |
quick check:
~/projects/halmos on code-fastpath wip *21 !2 ?50 ❯ python -m timeit --setup='import math' 'int(math.log(32, 2))'
2000000 loops, best of 5: 121 nsec per loop
~/projects/halmos on code-fastpath wip *21 !2 ?50 ❯ python -m timeit 'int(32).bit_length() - 1'
5000000 loops, best of 5: 66.1 nsec per loop
0xkarmacoma
reviewed
Aug 13, 2024
src/halmos/sevm.py
Outdated
| @@ -1348,7 +1356,35 @@ def arith(self, ex: Exec, op: int, w1: Word, w2: Word) -> Word: | |||
| return w1 - w2 | |||
|
|
|||
| if op == EVM.MUL: | |||
| return w1 * w2 | |||
| if is_bv_value(w1) and is_bv_value(w2): | |||
There was a problem hiding this comment.
can we invoke is_bv_value(x) once for each and reuse the results? in the worst case it results in 6 calls to that function, which itself makes more function calls
0xkarmacoma
reviewed
Aug 13, 2024
| @@ -1348,7 +1356,35 @@ def arith(self, ex: Exec, op: int, w1: Word, w2: Word) -> Word: | |||
| return w1 - w2 | |||
|
|
|||
| if op == EVM.MUL: | |||
| return w1 * w2 | |||
| if is_bv_value(w1) and is_bv_value(w2): | |||
| return w1 * w2 | |||
There was a problem hiding this comment.
just to double check: we're fine here in case of overflow?
There was a problem hiding this comment.
yes, and it's indeed intended.
0xkarmacoma
approved these changes
Aug 13, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Abstract multiplication in a similar way to division and modulo operations.
The actual bitvector multiplication is used when either argument is concrete. Also, when an argument is a power of two, the left-shift is used instead of multiplication.