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 BitVecExtract simplification for constant folding #2524

Merged
merged 5 commits into from
Jan 20, 2022

Conversation

Boyan-MILANOV
Copy link
Contributor

This PR fixes an SMT simplification pattern for BitVecExtract on constants.
The current implementation was ignoring the most significant bit of the extracted value.

@Boyan-MILANOV Boyan-MILANOV marked this pull request as ready for review January 20, 2022 15:18
Copy link
Contributor

@ekilmer ekilmer left a comment

Choose a reason for hiding this comment

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

LGTM!

@Boyan-MILANOV Boyan-MILANOV merged commit 9321100 into master Jan 20, 2022
@Boyan-MILANOV Boyan-MILANOV deleted the fix-extract-simplification branch January 20, 2022 17:07
Boyan-MILANOV added a commit that referenced this pull request Jan 21, 2022
* Fix BitVecExtract simplification for constant folding

* Lint

* Add test for extract constant folding

* Lint

* Test: pass BitVecExtract args with keywords
ekilmer added a commit that referenced this pull request Mar 3, 2022
* master: (35 commits)
  Switch to stable Black (#2536)
  Fix typo in Manticore.linux constructor docstring (#2535)
  Revert CI changes made in #2526
  Release Manticore 0.3.7 (#2526)
  Optimise forking when there is only 1 solution (#2527)
  Epoll Implementation (#2529)
  Split off ENDBR32/64 from CHESS branch (#2533)
  Update to crytic-compile 0.2.2 (#2530)
  Also ignore missing unicorn registers in the fallback emulator (#2531)
  x86 FXSAVE & FXRSTOR support (#2511)
  Fix `BitVecExtract` simplification for constant folding (#2524)
  Add pip-audit action workflow (#2513)
  Add EXPLICIT fork policy (#2514)
  Enforce crytic-compile==0.2.1 (#2512)
  Improve namedtuple definition (#2506)
  Add SMT simplifications for bitvec subtraction (#2504)
  Fix handling of the program base address in Linux (#2500)
  Bump Sphinx version to 4.3.0 (#2503)
  Solver Improvements (#2502)
  Improves `namedtuple` definition (#2501)
  ...
ekilmer added a commit that referenced this pull request Apr 21, 2022
* master:
  Switch to stable Black (#2536)
  Fix typo in Manticore.linux constructor docstring (#2535)
  Revert CI changes made in #2526
  Release Manticore 0.3.7 (#2526)
  Optimise forking when there is only 1 solution (#2527)
  Epoll Implementation (#2529)
  Split off ENDBR32/64 from CHESS branch (#2533)
  Update to crytic-compile 0.2.2 (#2530)
  Also ignore missing unicorn registers in the fallback emulator (#2531)
  x86 FXSAVE & FXRSTOR support (#2511)
  Fix `BitVecExtract` simplification for constant folding (#2524)
  Add pip-audit action workflow (#2513)
  Add EXPLICIT fork policy (#2514)
  Enforce crytic-compile==0.2.1 (#2512)
  Improve namedtuple definition (#2506)
  Add SMT simplifications for bitvec subtraction (#2504)
  Fix handling of the program base address in Linux (#2500)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants