diff --git a/clang/lib/Verify/Frontend/ASTConverter.cpp b/clang/lib/Verify/Frontend/ASTConverter.cpp index 3387ec0793..696db0c132 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.cpp +++ b/clang/lib/Verify/Frontend/ASTConverter.cpp @@ -107,6 +107,27 @@ static std::unique_ptr machineOperand(std::unique_ptr V, return std::make_unique(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 shiftLeft(std::unique_ptr L, + std::unique_ptr 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(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( + VBinOp::Shl, + std::make_unique(std::move(L), From, Unsigned, Loc), + std::move(R), Unsigned, Loc); + return std::make_unique(std::move(Shifted), Unsigned, Ty, Loc); +} + /// The exact value of an integer operand. static std::unique_ptr mathOperand(std::unique_ptr V) { if (!V || !V->Ty.isInt() || evaluatedIntMode(V.get()) == VIntMode::Math) @@ -4573,6 +4594,8 @@ std::unique_ptr 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(*Op, std::move(L), std::move(R), Ty, E->getExprLoc()); } @@ -5208,8 +5231,12 @@ ASTConverter::convertAssignmentValue(const BinaryOperator *Assignment) { std::make_unique(std::move(LHS), LHSSourceTy, LHSComputationTy, Assignment->getExprLoc()); } - std::unique_ptr Value = std::make_unique( - Op, std::move(LHS), std::move(RHS), ResultTy, Assignment->getExprLoc()); + std::unique_ptr Value = + Op == VBinOp::Shl + ? shiftLeft(std::move(LHS), std::move(RHS), ResultTy, + Assignment->getExprLoc(), Ctx) + : std::make_unique(Op, std::move(LHS), std::move(RHS), + ResultTy, Assignment->getExprLoc()); if (!sameRepresentation(ResultTy, TargetTy)) return std::make_unique(std::move(Value), ResultTy, TargetTy, Assignment->getExprLoc()); diff --git a/clang/test/Verify/suite/shift_language_mode.cpp b/clang/test/Verify/suite/shift_language_mode.cpp new file mode 100644 index 0000000000..19b45a3d71 --- /dev/null +++ b/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] diff --git a/docs/DESIGN.md b/docs/DESIGN.md index ac1b25db13..0ed71e248a 100644 --- a/docs/DESIGN.md +++ b/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`. diff --git a/website/source/language/integers.rst b/website/source/language/integers.rst index fedd5a2c19..afb583de8a 100644 --- a/website/source/language/integers.rst +++ b/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