ACD: 64-bit shift by 64 or more in local_extend_to - #541
Open
marcelwa wants to merge 1 commit into
Open
Conversation
ac_decomposition_impl::local_extend_to() replicates a truth table that really
depends on `real_num_vars` variables across the full `num_vars`-variable static
truth table. For real_num_vars < 6 it does so by folding the first word:
for ( auto i = real_num_vars; i < num_vars; ++i )
mask |= ( mask << ( 1 << i ) );
Once i reaches 6 the shift distance is 1 << 6 == 64, which is at least the width
of the 64-bit operand, so the shift has undefined behaviour. This is reached
whenever the cut being decomposed has more than six variables, i.e. in every
ordinary use of `if -K k -Z n` with k > 6; UBSan reports
ac_decomposition.hpp: runtime error: shift exponent 64 is too large for
64-bit type 'long unsigned int'
on, for example, `read adder.aig; strash; dch -f; if -K 11 -Z 6 -C 12`.
On x86 the shift is taken modulo 64 and the iteration happens to be a no-op, so
the observable behaviour today is correct, but that is not guaranteed by the
language and other targets shift in a saturating or unspecified way.
Variables 6 and above do not need the fold at all: the subsequent
std::fill() over the whole block array already replicates the word across every
block. Clamp the loop to the variables that live inside one word. No
behavioural change on x86.
Contributor
|
Marcel, thank you for the fixes! I will review them and merge soon. |
Author
|
You're welcome. Let me know if you have any questions or need any further information I can provide 🙂 |
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
The defect
In
src/map/if/acd/ac_decomposition.hpp,local_extend_toreplicates a truth-table word:maskis a 64-bit word, so fori >= 6the shift amount1 << iis at least 64. Shifting a 64-bit integer by 64 or more is undefined behaviour in C++, not a no-op — in practice x86 masks the count to 6 bits, somask << 64becomesmask << 0and the value silently doubles instead of being left alone.Variables 6 and above are already replicated by the
std::fillthat follows, so the loop only ever needs to cover the within-word variables.Reach
This is hit on every
if -K k -Z ninvocation withk > 6, i.e. on every use of the delay-driven ACD path with cuts wider than a word. Found with UBSan.Fix
Bound the loop at 6, with a comment recording why the tail is unnecessary rather than merely harmless.
Testing
Built clean.
if -K 10 -Z 6oncavlcis unchanged (nd = 121, lev = 4).Related: #539 (uninitialised
bestPermread in the same file) and #540 (lutpackassertion), both found while measuring this decomposer across the EPFL suite.