From 0f5951ab2c60481a1ada9c577dfc3703fa90d77b Mon Sep 17 00:00:00 2001 From: agentic-synthesis Date: Sat, 8 Aug 2026 09:50:02 +0200 Subject: [PATCH] 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. --- src/map/if/acd/ac_decomposition.hpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/map/if/acd/ac_decomposition.hpp b/src/map/if/acd/ac_decomposition.hpp index 8d5ddb5c4..f8c55bfd7 100644 --- a/src/map/if/acd/ac_decomposition.hpp +++ b/src/map/if/acd/ac_decomposition.hpp @@ -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 ) ); }