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

clang/lib/Verify/Frontend/ASTConverter.cpp

@@ -107,6 +107,27 @@ static std::unique_ptr<VExpr> machineOperand(std::unique_ptr<VExpr> V,
   return std::make_unique<VCastExpr>(std::move(V), From, To, Loc);
 }
 
+/// \p L shifted left by \p R. C++20 defines a signed left shift as the value
+/// congruent to L * 2^R modulo 2^N, which is the unsigned shift
+/// reinterpreted; before C++20 a negative or overflowing one is undefined.
+static std::unique_ptr<VExpr> shiftLeft(std::unique_ptr<VExpr> L,
+                                        std::unique_ptr<VExpr> R,
+                                        const VType &Ty, SourceLocation Loc,
+                                        const ASTContext &Ctx) {
+  if (!Ctx.getLangOpts().CPlusPlus20 || !Ty.isSignedInt() ||
+      Ty.IntMode != VIntMode::Machine || !sameRepresentation(L->Ty, Ty))
+    return std::make_unique<VBinOpExpr>(VBinOp::Shl, std::move(L), std::move(R),
+                                        Ty, Loc);
+  VType Unsigned = Ty;
+  Unsigned.IsSigned = false;
+  const VType From = L->Ty;
+  auto Shifted = std::make_unique<VBinOpExpr>(
+      VBinOp::Shl,
+      std::make_unique<VCastExpr>(std::move(L), From, Unsigned, Loc),
+      std::move(R), Unsigned, Loc);
+  return std::make_unique<VCastExpr>(std::move(Shifted), Unsigned, Ty, Loc);
+}
+
 /// The exact value of an integer operand.
 static std::unique_ptr<VExpr> mathOperand(std::unique_ptr<VExpr> V) {
   if (!V || !V->Ty.isInt() || evaluatedIntMode(V.get()) == VIntMode::Math)
@@ -4573,6 +4594,8 @@ std::unique_ptr<VExpr> ASTConverter::convertExprImpl(const Expr *E) {
         return nullptr;
       }
     }
+    if (*Op == VBinOp::Shl)
+      return shiftLeft(std::move(L), std::move(R), Ty, E->getExprLoc(), Ctx);
     return std::make_unique<VBinOpExpr>(*Op, std::move(L), std::move(R), Ty,
                                         E->getExprLoc());
   }
@@ -5208,8 +5231,12 @@ ASTConverter::convertAssignmentValue(const BinaryOperator *Assignment) {
         std::make_unique<VCastExpr>(std::move(LHS), LHSSourceTy,
                                     LHSComputationTy, Assignment->getExprLoc());
   }
-  std::unique_ptr<VExpr> Value = std::make_unique<VBinOpExpr>(
-      Op, std::move(LHS), std::move(RHS), ResultTy, Assignment->getExprLoc());
+  std::unique_ptr<VExpr> Value =
+      Op == VBinOp::Shl
+          ? shiftLeft(std::move(LHS), std::move(RHS), ResultTy,
+                      Assignment->getExprLoc(), Ctx)
+          : std::make_unique<VBinOpExpr>(Op, std::move(LHS), std::move(RHS),
+                                         ResultTy, Assignment->getExprLoc());
   if (!sameRepresentation(ResultTy, TargetTy))
     return std::make_unique<VCastExpr>(std::move(Value), ResultTy, TargetTy,
                                        Assignment->getExprLoc());

clang/test/Verify/suite/shift_language_mode.cpp

@@ -0,0 +1,79 @@
+// RUN: not %cpp-verify %s -- -std=c++17 2>&1 | FileCheck %s --check-prefixes=CHECK,CXX17
+// RUN: not %cpp-verify %s -- -std=c++20 2>&1 | FileCheck %s --check-prefixes=CHECK,CXX20
+//
+// C++20 defines a signed left shift as the value congruent to E1 * 2^E2
+// modulo 2^N. Before C++20 it is undefined for a negative E1 and for a value
+// that does not fit the corresponding unsigned type. In both, the amount must
+// lie below the width, and a right shift of a negative value is arithmetic
+// (before C++20 implementation-defined, and arithmetic in Clang).
+
+int neg_shift()
+  cppverify::post(cppverify::result == -2)
+{
+  int m = -1;
+  return m << 1;
+}
+// CXX17-DAG: error: verification failed: neg_shift [{{.*}}::shift@
+// CXX20-DAG: Verified: neg_shift [backend=z3]
+
+int neg_shift_assign()
+  cppverify::post(cppverify::result == -8)
+{
+  int m = -2;
+  m <<= 2;
+  return m;
+}
+// CXX17-DAG: error: verification failed: neg_shift_assign [{{.*}}::shift@
+// CXX20-DAG: Verified: neg_shift_assign [backend=z3]
+
+// 2 * 2^31 fits neither int nor unsigned int; modulo 2^32 it is 0.
+int past_unsigned(int x)
+  cppverify::pre(x == 2)
+  cppverify::post(cppverify::result == 0)
+{
+  return x << 31;
+}
+// CXX17-DAG: error: verification failed: past_unsigned [{{.*}}::shift@
+// CXX20-DAG: Verified: past_unsigned [backend=z3]
+
+// A contract is C++ too.
+int doubled(int x)
+  cppverify::pre(x == -4)
+  cppverify::post(cppverify::result == (x << 1))
+{
+  return x * 2;
+}
+// CXX17-DAG: error: verification failed: doubled [{{.*}}::shift@
+// CXX20-DAG: Verified: doubled [backend=z3]
+
+// 2^31 fits unsigned int, so this is INT_MIN in both.
+int sign_bit()
+  cppverify::post(cppverify::result == -2147483647 - 1)
+{
+  int one = 1;
+  return one << 31;
+}
+// CHECK-DAG: Verified: sign_bit [backend=z3]
+
+int too_far(int x, int k)
+  cppverify::pre(x == 1 && k == 32)
+{
+  return x << k;
+}
+// CHECK-DAG: error: verification failed: too_far [{{.*}}::shift@
+
+int neg_right()
+  cppverify::post(cppverify::result == -2)
+{
+  int m = -3;
+  return m >> 1;
+}
+// CHECK-DAG: Verified: neg_right [backend=z3]
+
+unsigned wraps()
+  cppverify::post(cppverify::result == 0)
+{
+  unsigned u = 2;
+  return u << 31;
+}
+// CHECK-DAG: Verified: wraps [backend=z3]

docs/DESIGN.md

@@ -671,7 +671,10 @@ wraps, and signed overflow is undefined. The verifier uses machine-integer
 values but unfolds the function into the path-sensitive definedness checker at every call;
 an overflowing call is rejected rather than interpreted as signed wraparound.
 For C++17 signed left shift, a nonnegative value may set the sign bit when the
-shifted mathematical value fits the corresponding unsigned type.
+shifted mathematical value fits the corresponding unsigned type. From C++20
+(`-std=c++20`), a signed left shift is the value congruent to `E1 * 2^E2`
+modulo `2^N`, as the standard defines, and only its amount must lie below the
+width.
 
 **Contrast with explicit `cppverify::spec`:** `cppverify::spec int fibo(int n)` uses mathematical integers (Z3 `Int`, unbounded). Users pick:
 - Want fast verification with abstract math semantics → write `cppverify::spec`.

website/source/language/integers.rst

@@ -87,7 +87,8 @@ Core checks include:
    * - signed ``/`` ``%``
      - not ``INT_MIN / -1`` (which overflows)
    * - ``<<`` and ``>>``
-     - shift count is in range; signed left shift satisfies the C++17 rule
+     - shift count is in range; before C++20, signed left shift satisfies the
+       C++17 rule
    * - pointer loads and stores
      - base pointer is non-null and abstractly valid
    * - mathematical value converted to a machine type
@@ -153,10 +154,13 @@ verifier unfolds the body for C++ definedness checks, so signed overflow, invali
 shifts, and division undefined behavior cannot be justified by machine
 wraparound.
 
-Signed left shift follows the C++17 rule: the left operand must be nonnegative
-and the shifted value must fit the corresponding unsigned type.  This permits
-constructing the sign bit (for example, ``1 << 31`` for a 32-bit ``int``) while
-still rejecting values beyond the unsigned range.
+Before C++20, signed left shift follows the C++17 rule: the left operand must
+be nonnegative and the shifted value must fit the corresponding unsigned type.
+This permits constructing the sign bit (for example, ``1 << 31`` for a 32-bit
+``int``) while still rejecting values beyond the unsigned range. From C++20
+(``-std=c++20``), a signed left shift is the value congruent to
+``E1 * 2^E2`` modulo ``2^N``, as the standard defines, so ``-1 << 1`` is
+``-2``; only the shift count must be in range.
 
 Calls crossing between mathematical ``cppverify::spec`` code and lifted machine
 ``constexpr`` code convert at each parameter and return boundary. A machine