Skip to content

verify: Define a signed left shift modulo 2^N from C++20 - #20

Merged
SwayamInSync merged 4 commits into
mainfrom
fix/cxx20-shifts
Oct 14, 2026
Merged

SwayamInSync merged 4 commits into
mainfrom
fix/cxx20-shifts

Conversation

@SwayamInSync

Copy link
Copy Markdown
Owner

C++20 defines E1 << E2 for a signed E1 as the value congruent to E1 * 2^E2 modulo 2^N ([expr.shift]/2); before C++20 it is undefined for a negative E1 and for a value that does not fit the unsigned type. The verifier applied the C++17 rule under every -std, so with -std=c++20

int neg_shift()
  cppverify::post(cppverify::result == -2)
{
  int m = -1;
  return m << 1;
}

failed a shift check that C++20 does not have.

From C++20 the converter lowers a signed left shift as the unsigned shift, reinterpreted, which is exactly the standard's value; the passivizer then checks only that the amount is below the width. Earlier modes, and right shifts (arithmetic in both, implementation-defined before C++20 and arithmetic in Clang), are unchanged. The language mode is the frontend's to decide, so no other layer changes.

Testing: suite/shift_language_mode.cpp runs every rule under -std=c++17 and -std=c++20 and fails on main under C++20. Lowering in every mode breaks the C++17 checks, and leaving out the compound assignment breaks m <<= 2. Verify suite: 398 passed, 1 unsupported; it runs as C++17, where the converter builds the same shift as before. Under -std=c++20, a verdict differential against main over the 12 Verify sources with shifts changes only the tests of C++17's undefined signed shifts, unsafe_signed_left_negative, unsafe_signed_left_overflow, and unsafe_i128_left_shift, which now verify; decode_uleb128_length_11, whose shifts are all unsigned, timed out under load in that run.

@SwayamInSync
SwayamInSync merged commit ec14e8e into main Oct 14, 2026
14 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant