ACD: avoid a 64-bit shift by 64 or more in local_extend_to

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.
This commit is contained in:
agentic-synthesis 2026-08-08 09:50:02 +02:00
parent 8e224cd794
commit 0f5951ab2c
No known key found for this signature in database
GPG Key ID: 2979DB71A0C2C23D
1 changed files with 4 additions and 1 deletions

View File

@ -1317,7 +1317,10 @@ private:
{
auto mask = *tt.begin();
for ( auto i = real_num_vars; i < num_vars; ++i )
/* Replicate within the word only. Variables 6 and above are replicated by the
* std::fill below, and shifting a 64-bit word by (1 << i) for i >= 6 is undefined
* behaviour rather than a no-op. */
for ( auto i = real_num_vars; i < std::min( num_vars, 6u ); ++i )
{
mask |= ( mask << ( 1 << i ) );
}