diff --git a/clang/lib/Headers/cppverify.h b/clang/lib/Headers/cppverify.h index 3199d74f8a..08eef3da24 100644 --- a/clang/lib/Headers/cppverify.h +++ b/clang/lib/Headers/cppverify.h @@ -218,6 +218,93 @@ struct map { }; map map_empty(); +/* The meaning the verifier gives to the C library's memcpy, memmove, memset, + * and memcmp. A call with pointers to an integer type T, written before their + * conversion to void *, and a size of k * sizeof(T) bytes is a call of the + * model for T with k: whole objects, which keep their values bit for bit. + * The models are trusted: a proof that uses one names it in [trusts=...]. + * Distinct pointer parameters of which one is mutable address separate + * objects (memcpy's ranges must not overlap); memmove's may overlap. */ +namespace model { + +#define __CPPVERIFY_MEMORY_MODELS(T) \ + [[cppverify::trusted]] T *memcpy(T *d, const T *s, __SIZE_TYPE__ k) \ + cppverify::pre(cppverify::valid(d, k) && cppverify::valid(s, k)) \ + cppverify::modifies(d[0 : k]) \ + cppverify::post(cppverify::forall(i, 0, k, d[i] == cppverify::old(s[i])))\ + cppverify::post(cppverify::result == d); \ + [[cppverify::trusted]] T *memmove(T *d, const T *s, __SIZE_TYPE__ k) \ + cppverify::aliases(d, s) \ + cppverify::pre(cppverify::valid(d, k) && cppverify::valid(s, k)) \ + cppverify::modifies(d[0 : k]) \ + cppverify::post(cppverify::forall(i, 0, k, d[i] == cppverify::old(s[i])))\ + cppverify::post(cppverify::result == d); + +/* memset(d, c, n) stores the byte (unsigned char)c in every byte: v is that + * byte repeated in an object of type T. */ +#define __CPPVERIFY_MEMSET_MODEL(T) \ + [[cppverify::trusted]] T *memset(T *d, T v, __SIZE_TYPE__ k) \ + cppverify::pre(cppverify::valid(d, k)) \ + cppverify::modifies(d[0 : k]) \ + cppverify::post(cppverify::forall(i, 0, k, d[i] == v)) \ + cppverify::post(cppverify::result == d); + +/* memcmp is 0 exactly when the objects are equal. Of bytes, its sign is that + * of the first difference, as unsigned char; of wider objects that depends + * on the byte order, and only equality is modeled. */ +#define __CPPVERIFY_MEMCMP_MODEL(T) \ + [[cppverify::trusted]] int memcmp(const T *a, const T *b, __SIZE_TYPE__ k) \ + cppverify::pre(cppverify::valid(a, k) && cppverify::valid(b, k)) \ + cppverify::post((cppverify::result == 0) == \ + cppverify::forall(i, 0, k, a[i] == b[i])); +#define __CPPVERIFY_BYTE_MEMCMP_MODEL(T) \ + [[cppverify::trusted]] int memcmp(const T *a, const T *b, __SIZE_TYPE__ k) \ + cppverify::pre(cppverify::valid(a, k) && cppverify::valid(b, k)) \ + cppverify::post((cppverify::result == 0) == \ + cppverify::forall(i, 0, k, a[i] == b[i])) \ + cppverify::post(cppverify::forall( \ + j, 0, k, \ + !cppverify::forall(i, 0, j, a[i] == b[i]) || a[j] == b[j] || \ + (cppverify::result < 0) == \ + ((a[j] & 255) < (b[j] & 255)))); + +#define __CPPVERIFY_WIDE_MODELS(T) \ + __CPPVERIFY_MEMORY_MODELS(T) \ + __CPPVERIFY_MEMSET_MODEL(T) \ + __CPPVERIFY_MEMCMP_MODEL(T) +#define __CPPVERIFY_BYTE_MODELS(T) \ + __CPPVERIFY_MEMORY_MODELS(T) \ + __CPPVERIFY_MEMSET_MODEL(T) \ + __CPPVERIFY_BYTE_MEMCMP_MODEL(T) + +__CPPVERIFY_MEMORY_MODELS(bool) +__CPPVERIFY_MEMCMP_MODEL(bool) +__CPPVERIFY_BYTE_MODELS(char) +__CPPVERIFY_BYTE_MODELS(signed char) +__CPPVERIFY_BYTE_MODELS(unsigned char) +__CPPVERIFY_WIDE_MODELS(wchar_t) +#if __cplusplus >= 201103L +__CPPVERIFY_WIDE_MODELS(char16_t) +__CPPVERIFY_WIDE_MODELS(char32_t) +#endif +__CPPVERIFY_WIDE_MODELS(short) +__CPPVERIFY_WIDE_MODELS(unsigned short) +__CPPVERIFY_WIDE_MODELS(int) +__CPPVERIFY_WIDE_MODELS(unsigned) +__CPPVERIFY_WIDE_MODELS(long) +__CPPVERIFY_WIDE_MODELS(unsigned long) +__CPPVERIFY_WIDE_MODELS(long long) +__CPPVERIFY_WIDE_MODELS(unsigned long long) + +#undef __CPPVERIFY_MEMORY_MODELS +#undef __CPPVERIFY_MEMSET_MODEL +#undef __CPPVERIFY_MEMCMP_MODEL +#undef __CPPVERIFY_BYTE_MEMCMP_MODEL +#undef __CPPVERIFY_WIDE_MODELS +#undef __CPPVERIFY_BYTE_MODELS + +} // namespace model + } // namespace cppverify #endif /* __cplusplus */ diff --git a/clang/lib/Verify/Backend/Obligation.cpp b/clang/lib/Verify/Backend/Obligation.cpp index 990ffa2e28..0044a1c04a 100644 --- a/clang/lib/Verify/Backend/Obligation.cpp +++ b/clang/lib/Verify/Backend/Obligation.cpp @@ -276,6 +276,8 @@ ObligationKind verify::obligationKind(ProofObligationKind Kind) { return ObligationKind::MissingReturn; case ProofObligationKind::Unreachable: return ObligationKind::Unreachable; + case ProofObligationKind::BuiltinArgument: + return ObligationKind::BuiltinArgument; case ProofObligationKind::Unsupported: return ObligationKind::Unsupported; } @@ -328,6 +330,8 @@ const char *verify::obligationKindName(ObligationKind Kind) { return "missing-return"; case ObligationKind::Unreachable: return "unreachable"; + case ObligationKind::BuiltinArgument: + return "builtin-argument"; case ObligationKind::Unsupported: return "unsupported"; } @@ -2515,12 +2519,13 @@ class ObligationBuilder { Stmt->Focus, Stmt->Clause}); } - std::vector< - std::tuple, std::string>> + std::vector, + std::string, SourceSpan>> ExitAsserts; for (const PassiveExitAssert &Exit : P.ExitAsserts) ExitAsserts.emplace_back(obligationKind(Exit.ProofKind), - fromVExpr(Exit.Cond.get()), Exit.Note); + fromVExpr(Exit.Cond.get()), Exit.Note, + Exit.Anchor); // A theorem only where it speaks of the entry state alone: the body's // later states are not part of it. @@ -2594,22 +2599,27 @@ class ObligationBuilder { auto appendObligation = [&](ObligationKind Kind, const VCExpr *Condition, uint64_t TraceEventCount, const std::string &Note = "", - SourceSpan Focus = {}, SourceSpan Clause = {}) { + SourceSpan Focus = {}, SourceSpan Clause = {}, + SourceSpan Anchor = {}) { Obligation Item; Item.Kind = Kind; Item.Note = Note; Item.Focus = Focus; Item.Clause = Clause; - Item.Loc = Condition->Loc; - Item.BeginLoc = Condition->BeginLoc; - Item.EndLoc = Condition->EndLoc; + if (Anchor.isValid()) + Item.Focus = {Condition->Loc, Condition->BeginLoc, Condition->EndLoc}; + else + Anchor = {Condition->Loc, Condition->BeginLoc, Condition->EndLoc}; + Item.Loc = Anchor.Loc; + Item.BeginLoc = Anchor.BeginLoc; + Item.EndLoc = Anchor.EndLoc; Item.TraceEventCount = TraceEventCount; Item.Id = Identity + "::obligation:" + std::to_string(++ObligationIndex); Item.Goal = makeGoal(Condition); Item.CounterexampleQuery = vcNot(cloneLogicExpr(Item.Goal.get())); - Item.CounterexampleQuery->Loc = Condition->Loc; - Item.CounterexampleQuery->BeginLoc = Condition->BeginLoc; - Item.CounterexampleQuery->EndLoc = Condition->EndLoc; + Item.CounterexampleQuery->Loc = Anchor.Loc; + Item.CounterexampleQuery->BeginLoc = Anchor.BeginLoc; + Item.CounterexampleQuery->EndLoc = Anchor.EndLoc; M.Obligations.push_back(std::move(Item)); }; @@ -2625,8 +2635,9 @@ class ObligationBuilder { if (oversize()) return ObligationSizeError::obligations(size(), MaxNodes); } - for (const auto &[Kind, Exit, Note] : ExitAsserts) { - appendObligation(Kind, Exit.get(), M.TraceEvents.size(), Note); + for (const auto &[Kind, Exit, Note, Anchor] : ExitAsserts) { + appendObligation(Kind, Exit.get(), M.TraceEvents.size(), Note, {}, {}, + Anchor); if (oversize()) return ObligationSizeError::obligations(size(), MaxNodes); } diff --git a/clang/lib/Verify/Backend/Obligation.h b/clang/lib/Verify/Backend/Obligation.h index e07eed7012..aeda280a3a 100644 --- a/clang/lib/Verify/Backend/Obligation.h +++ b/clang/lib/Verify/Backend/Obligation.h @@ -285,6 +285,7 @@ enum class ObligationKind { Deallocation, MissingReturn, Unreachable, + BuiltinArgument, Unsupported }; diff --git a/clang/lib/Verify/Backend/ObligationSerialization.cpp b/clang/lib/Verify/Backend/ObligationSerialization.cpp index c35c8edb17..7ffada4eae 100644 --- a/clang/lib/Verify/Backend/ObligationSerialization.cpp +++ b/clang/lib/Verify/Backend/ObligationSerialization.cpp @@ -329,6 +329,8 @@ uint8_t obligationTag(ObligationKind Kind) { return 21; case ObligationKind::Unreachable: return 23; + case ObligationKind::BuiltinArgument: + return 24; case ObligationKind::Unsupported: return 22; } @@ -386,6 +388,10 @@ std::optional obligationFromTag(uint8_t Tag, uint32_t Version) { return ObligationKind::Unsupported; case 23: return ObligationKind::Unreachable; + case 24: + if (Version < 6) + return std::nullopt; + return ObligationKind::BuiltinArgument; default: return std::nullopt; } diff --git a/clang/lib/Verify/Driver/Counterexample.cpp b/clang/lib/Verify/Driver/Counterexample.cpp index f9a2bb9a25..64a70c8d4e 100644 --- a/clang/lib/Verify/Driver/Counterexample.cpp +++ b/clang/lib/Verify/Driver/Counterexample.cpp @@ -193,6 +193,7 @@ bool isDefinedness(ObligationKind Kind) { case ObligationKind::Initialization: case ObligationKind::PointerDifference: case ObligationKind::PointerValidity: + case ObligationKind::BuiltinArgument: return true; default: return false; @@ -289,8 +290,7 @@ FailurePlace verify::failingPlace(const ObligationModule &Module, return nullptr; } if (Generated && E->K == LogicExpr::Or && E->Children.size() == 2 && - E->Children[0]->K == LogicExpr::Not && isFalse(E->Children[0].get()) && - isFalse(E->Children[1].get())) + isFalse(E->Children[0].get()) && isFalse(E->Children[1].get())) if (const LogicExpr *Part = falsePart(E->Children[1].get())) return Part; return placed(E) ? E : nullptr; diff --git a/clang/lib/Verify/Frontend/ASTConverter.cpp b/clang/lib/Verify/Frontend/ASTConverter.cpp index 9b7da0c844..72fa28b54f 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.cpp +++ b/clang/lib/Verify/Frontend/ASTConverter.cpp @@ -745,6 +745,9 @@ findUnsupportedType(const FunctionDecl *FD, bool AllowScalarReferences, : AllowScalarReferences(AllowScalarReferences) {} bool VisitExpr(Expr *E) { + // A static_assert's message has no type. + if (E->getType().isNull()) + return true; if (const auto *ICE = dyn_cast(E)) if (ICE->getCastKind() == CK_FunctionToPointerDecay || ICE->getCastKind() == CK_BuiltinFnToFnPtr) @@ -946,6 +949,16 @@ VIntMode ASTConverter::specCallIntMode(const FunctionDecl *FD) const { return VIntMode::Math; } +/// Whether \p FD is a model of , in cppverify::model. +static bool isLibraryModel(const FunctionDecl *FD) { + const auto *Model = dyn_cast(FD->getDeclContext()); + const auto *Verify = + Model ? dyn_cast(Model->getDeclContext()) : nullptr; + return Verify && Model->getName() == "model" && + Verify->getName() == "cppverify" && + Verify->getDeclContext()->isTranslationUnit(); +} + /// For std::min(a, b) and std::max(a, b) of two integers, enumerations, or /// bools: whether it is max. Nothing for any other function, such as the /// overloads with a comparison or an initializer list. @@ -2445,7 +2458,7 @@ std::vector> ASTConverter::convertTranslationUnit() { FD->getQualifiedNameAsString() + ": " + *UnsupportedMember); continue; } - if (FD->isInStdNamespace()) + if (FD->isInStdNamespace() || isLibraryModel(FD)) continue; if (FD->isTemplateInstantiation()) { // Its diagnostics note where it is instantiated, as a compiler's do, @@ -2499,6 +2512,14 @@ std::vector> ASTConverter::convertTranslationUnit() { }; Calls(FD->getBody()); } + // The models the converted calls use, trusted by their callers, and quiet: + // the others are never converted. + for (const FunctionDecl *Model : UsedLibraryModels) + if (auto Fn = convertFunction(Model)) { + Fn->IsBuiltin = true; + Identities.insert(Fn->Identity); + Out.push_back(std::move(Fn)); + } // An uncontracted constexpr definition is a spec once the lowered code // calls it: lift those the converted functions call, then those the lifted // ones call, in source order. The others (a header's, say) are never @@ -4135,8 +4156,7 @@ ASTConverter::convertLoopCondition(const Stmt *Loop, const Expr *Cond, return std::make_unique(false, VType::makeBool(), Cond->getExprLoc()); llvm::SaveAndRestore Sink(CallSink, Calls); - llvm::SaveAndRestore Hoisted(HoistedCalls, - std::map()); + llvm::SaveAndRestore Hoisted(HoistedValues, decltype(HoistedValues)()); return convertExpr(Cond); } @@ -4337,6 +4357,393 @@ std::unique_ptr ASTConverter::convertMinOrMax(const CallExpr *CE, std::move(A), Ty, Loc); } +const FunctionDecl *ASTConverter::libraryModel(llvm::StringRef Name, + QualType Element) const { + auto nested = [&](const DeclContext *DC, + llvm::StringRef Inner) -> const NamespaceDecl * { + for (const NamedDecl *D : DC->lookup(&Ctx.Idents.get(Inner))) + if (const auto *NS = dyn_cast(D)) + return NS; + return nullptr; + }; + const NamespaceDecl *Verify = + nested(Ctx.getTranslationUnitDecl(), "cppverify"); + const NamespaceDecl *Model = Verify ? nested(Verify, "model") : nullptr; + if (!Model) + return nullptr; + for (const NamedDecl *D : Model->lookup(&Ctx.Idents.get(Name))) + if (const auto *FD = dyn_cast(D); + FD && FD->getNumParams() == 3 && + Ctx.hasSameUnqualifiedType( + FD->getParamDecl(0)->getType()->getPointeeType(), Element)) + return FD; + return nullptr; +} + +/// A pointer argument as written, before its conversion to (const) void *. +static const Expr *beforeVoidPointer(const Expr *E) { + E = E->IgnoreParens(); + while (const auto *Cast = dyn_cast(E)) { + if (Cast->getCastKind() != CK_BitCast && Cast->getCastKind() != CK_NoOp) + break; + E = Cast->getSubExpr()->IgnoreParens(); + } + return E; +} + +std::optional +ASTConverter::convertLibraryCall(const CallExpr *CE, + std::vector> &Out, + const std::string &Result) { + llvm::StringRef Name; + unsigned Pointers = 2; + switch (CE->getBuiltinCallee()) { + case Builtin::BImemcpy: + case Builtin::BI__builtin_memcpy: + Name = "memcpy"; + break; + case Builtin::BImemmove: + case Builtin::BI__builtin_memmove: + Name = "memmove"; + break; + case Builtin::BImemset: + case Builtin::BI__builtin_memset: + Name = "memset"; + Pointers = 1; + break; + case Builtin::BImemcmp: + case Builtin::BI__builtin_memcmp: + Name = "memcmp"; + break; + default: + return std::nullopt; + } + if (CE->getNumArgs() != 3) + return std::nullopt; + const SourceLocation Loc = CE->getExprLoc(); + // The objects a pointer addresses as written; an enumeration's are its + // underlying integers. + auto element = [&](const Expr *Arg) -> QualType { + QualType T = beforeVoidPointer(Arg)->getType(); + if (!T->isPointerType()) + return QualType(); + T = T->getPointeeType().getCanonicalType().getUnqualifiedType(); + if (const auto *Enum = T->getAs()) + T = Enum->getDecl()->getIntegerType().getCanonicalType(); + return T->isIntegerType() ? T : QualType(); + }; + const QualType Element = element(CE->getArg(0)); + // Objects of one size keep their bits; a bool holds only 0 or 1. + const FunctionDecl *Model = nullptr; + if (!Element.isNull()) { + const QualType Other = Pointers == 2 ? element(CE->getArg(1)) : Element; + if (!Other.isNull() && Ctx.getTypeSize(Other) == Ctx.getTypeSize(Element) && + Other->isBooleanType() == Element->isBooleanType()) + Model = libraryModel(Name, Element); + } + if (!Model) { + std::string Written; + llvm::raw_string_ostream OS(Written); + for (unsigned I = 0; I < Pointers; ++I) + OS << (I ? " and " : "") << "'" + << beforeVoidPointer(CE->getArg(I)) + ->getType() + .getAsString(Ctx.getPrintingPolicy()) + << "'"; + error(CurrentFn->Name + ": " + Name.str() + " of " + Written + + " is unsupported: it is modeled for pointers to integers of one " + "size" + + (Name == "memset" ? " other than bool" : "")); + return nullptr; + } + for (unsigned I = 0; I < 3; ++I) + for (unsigned J = I + 1; J < 3; ++J) + if (orderDependent(CE->getArg(I), CE->getArg(J))) { + error(CurrentFn->Name + + ": C++ leaves the order of these call arguments open, and a " + "call or a write in one may change what another reads; make it " + "a statement of its own first"); + return nullptr; + } + llvm::SaveAndRestore Sink(CallSink, &Out); + std::vector> Args; + for (unsigned I = 0; I < 3; ++I) { + auto Arg = convertExpr(I < Pointers ? beforeVoidPointer(CE->getArg(I)) + : CE->getArg(I)); + if (!Arg) + return nullptr; + Args.push_back(std::move(Arg)); + } + if (Name == "memset") { + // Each byte is (unsigned char)c, so each object is that byte repeated. + const uint64_t Width = Ctx.getTypeSize(Element); + const VType Object = VType::fromQualType(Element, VIntMode::Machine, Ctx); + const VType Byte = + VType::fromQualType(Ctx.UnsignedCharTy, VIntMode::Machine, Ctx); + VType Bits = Object; + Bits.IsSigned = false; + const VType Given = Args[1]->Ty; + std::unique_ptr Value = + std::make_unique(std::move(Args[1]), Given, Byte, Loc); + Value = std::make_unique(std::move(Value), Byte, Bits, Loc); + llvm::APInt Repeated(Width, 0); + for (uint64_t Bit = 0; Bit < Width; Bit += 8) + Repeated.setBit(Bit); + Value = std::make_unique( + VBinOp::Mul, std::move(Value), + std::make_unique(llvm::toString(Repeated, 10, false), + Bits, Loc), + Bits, Loc); + Args[1] = std::make_unique(std::move(Value), Bits, Object, Loc); + } + // Whole objects only: a size that splits one is defined C++ that the + // verifier's memory, an object to a cell, does not represent. + const uint64_t Size = Ctx.getTypeSizeInChars(Element).getQuantity(); + if (Size != 1) { + const VType SizeTy = Args[2]->Ty; + auto literal = [&](uint64_t V) { + return std::make_unique(std::to_string(V), SizeTy, Loc); + }; + Out.push_back(std::make_unique( + std::make_unique( + VBinOp::Eq, + std::make_unique(VBinOp::Rem, cloneVExpr(Args[2].get()), + literal(Size), SizeTy, Loc), + literal(0), VType::makeBool(), Loc), + Loc, ProofObligationKind::Unsupported, + Name.str() + " of a size that splits an object")); + Args[2] = std::make_unique(VBinOp::Div, std::move(Args[2]), + literal(Size), SizeTy, Loc); + } + if (!llvm::is_contained(UsedLibraryModels, Model)) + UsedLibraryModels.push_back(Model); + Out.push_back(atCall( + std::make_unique(functionName(Model), functionIdentity(Model), + std::move(Args), Result, Loc, false), + CE)); + return Model; +} + +std::optional> +ASTConverter::convertAbs(const CallExpr *CE) { + switch (CE->getBuiltinCallee()) { + case Builtin::BIabs: + case Builtin::BIlabs: + case Builtin::BIllabs: + case Builtin::BI__builtin_abs: + case Builtin::BI__builtin_labs: + case Builtin::BI__builtin_llabs: + break; + default: { + // std::abs of an integer, which a library may define inline: in std + // (libstdc++), or, for long and long long, in the global namespace of + // its , which brings into std (libc++). A global abs + // of the user's own is a function like any other. + const FunctionDecl *Callee = CE->getDirectCallee(); + if (!Callee || + !(Callee->isInStdNamespace() || + (Callee->getDeclContext()->getRedeclContext()->isTranslationUnit() && + Ctx.getSourceManager().isInSystemHeader(Callee->getLocation()))) || + !Callee->getIdentifier() || + Callee->getName() != "abs" || Callee->getNumParams() != 1 || + !Callee->getParamDecl(0)->getType()->isIntegerType() || + !Ctx.hasSameType(Callee->getParamDecl(0)->getType(), + Callee->getReturnType())) + return std::nullopt; + } + } + if (CE->getNumArgs() != 1) + return std::nullopt; + // In a spec the mathematical absolute value; elsewhere a function of + // machine integers, in a contract too, where -x overflows at the minimum. + const VType Parameter = + VType::fromQualType(CE->getArg(0)->getType(), IntMode, Ctx); + if (!Parameter.isInt() || !Parameter.IsSigned) + return std::nullopt; + auto Arg = convertExpr(CE->getArg(0)); + if (!Arg) + return nullptr; + const SourceLocation Loc = CE->getExprLoc(); + const VType Given = Arg->Ty; + if (evaluatedIntMode(Arg.get()) != Parameter.IntMode || + Given.BitWidth != Parameter.BitWidth) + Arg = std::make_unique(std::move(Arg), Given, Parameter, Loc); + auto Negative = std::make_unique( + VBinOp::Lt, cloneVExpr(Arg.get()), + std::make_unique("0", Parameter, Loc), VType::makeBool(), + Loc); + auto Negated = std::make_unique( + VUnaryOp::Neg, cloneVExpr(Arg.get()), Parameter, Loc); + std::unique_ptr Value = std::make_unique( + std::move(Negative), std::move(Negated), std::move(Arg), Parameter, Loc); + const VType Result = VType::fromQualType(CE->getType(), IntMode, Ctx); + if (!sameRepresentation(Parameter, Result)) + Value = + std::make_unique(std::move(Value), Parameter, Result, Loc); + return Value; +} + +std::optional> +ASTConverter::convertBitBuiltin(const CallExpr *CE) { + enum { Clz, Ctz, Popcount, Parity, Ffs, Bswap } Op; + switch (CE->getBuiltinCallee()) { + case Builtin::BI__builtin_clz: + case Builtin::BI__builtin_clzl: + case Builtin::BI__builtin_clzll: + Op = Clz; + break; + case Builtin::BI__builtin_ctz: + case Builtin::BI__builtin_ctzl: + case Builtin::BI__builtin_ctzll: + Op = Ctz; + break; + case Builtin::BI__builtin_popcount: + case Builtin::BI__builtin_popcountl: + case Builtin::BI__builtin_popcountll: + Op = Popcount; + break; + case Builtin::BI__builtin_parity: + case Builtin::BI__builtin_parityl: + case Builtin::BI__builtin_parityll: + Op = Parity; + break; + case Builtin::BI__builtin_ffs: + case Builtin::BI__builtin_ffsl: + case Builtin::BI__builtin_ffsll: + Op = Ffs; + break; + case Builtin::BI__builtin_bswap16: + case Builtin::BI__builtin_bswap32: + case Builtin::BI__builtin_bswap64: + Op = Bswap; + break; + default: + return std::nullopt; + } + if (CE->getNumArgs() != 1) + return std::nullopt; + auto Arg = convertExpr(CE->getArg(0)); + if (!Arg) + return nullptr; + const SourceLocation Loc = CE->getExprLoc(); + // The definitions read the operand's bits as an unsigned machine value, + // through comparisons with constants, conditionals, and sums without + // carries, so that no operation of them has a definedness check of its + // own; a mathematical operand converts, as a bitwise operand does. + const VType Parameter = + VType::fromQualType(CE->getArg(0)->getType(), VIntMode::Machine, Ctx); + if ((Parameter.Kind != VTypeKind::Int32 && + Parameter.Kind != VTypeKind::Int64) || + Parameter.BitWidth == 0 || Parameter.BitWidth > 64) + return std::nullopt; + const VType Given = Arg->Ty; + if (evaluatedIntMode(Arg.get()) != Parameter.IntMode || + Given.IsSigned != Parameter.IsSigned || + Given.BitWidth != Parameter.BitWidth) + Arg = std::make_unique(std::move(Arg), Given, Parameter, Loc); + VType Bits = Parameter; + Bits.IsSigned = false; + if (Parameter.IsSigned) + Arg = std::make_unique(std::move(Arg), Parameter, Bits, Loc); + const unsigned Width = Bits.BitWidth; + const VType Result = VType::fromQualType(CE->getType(), IntMode, Ctx); + auto power = [&](unsigned K) { + return llvm::toString(llvm::APInt::getOneBitSet(Width, K), 10, false); + }; + auto literal = [&](const std::string &Value, const VType &Ty) { + return std::make_unique(Value, Ty, Loc); + }; + auto bitSet = [&](unsigned K) -> std::unique_ptr { + return std::make_unique( + VBinOp::Ne, + std::make_unique(VBinOp::BitAnd, cloneVExpr(Arg.get()), + literal(power(K), Bits), Bits, Loc), + literal("0", Bits), VType::makeBool(), Loc); + }; + // Term(K) for each set bit K, of type Ty, combined by Op in a balanced + // tree. + auto overBits = [&](VBinOp Combine, const VType &Ty, + llvm::function_ref Term) { + std::vector> Terms; + for (unsigned K = 0; K != Width; ++K) + Terms.push_back(std::make_unique( + bitSet(K), literal(Term(K), Ty), literal("0", Ty), Ty, Loc)); + while (Terms.size() > 1) { + std::vector> Pairs; + for (size_t I = 0; I + 1 < Terms.size(); I += 2) + Pairs.push_back(std::make_unique( + Combine, std::move(Terms[I]), std::move(Terms[I + 1]), Ty, Loc)); + if (Terms.size() % 2) + Pairs.push_back(std::move(Terms.back())); + Terms = std::move(Pairs); + } + return std::move(Terms.front()); + }; + std::unique_ptr Value; + switch (Op) { + case Clz: + // The highest set bit decides; 0 has Width leading zeros, as C++20's + // std::countl_zero. + Value = literal(std::to_string(Width), Result); + for (unsigned K = 0; K != Width; ++K) + Value = std::make_unique( + bitSet(K), literal(std::to_string(Width - 1 - K), Result), + std::move(Value), Result, Loc); + break; + case Ctz: + case Ffs: + // The lowest set bit decides; 0 has Width trailing zeros, and ffs(0) + // is 0. + Value = literal(Op == Ctz ? std::to_string(Width) : "0", Result); + for (unsigned K = Width; K-- != 0;) + Value = std::make_unique( + bitSet(K), literal(std::to_string(Op == Ctz ? K : K + 1), Result), + std::move(Value), Result, Loc); + break; + case Popcount: + case Parity: { + // At most 64, so the count is summed in a byte, whose adders are small. + const VType Byte = + VType::fromQualType(Ctx.UnsignedCharTy, VIntMode::Machine, Ctx); + auto Count = overBits(VBinOp::Add, Byte, + [](unsigned) { return std::string("1"); }); + if (Op == Parity) + Count = std::make_unique(VBinOp::BitAnd, std::move(Count), + literal("1", Byte), Byte, Loc); + Value = std::make_unique(std::move(Count), Byte, Result, Loc); + break; + } + case Bswap: + // Each bit moves to its own place, so the bits combine without carries. + if (Width % 8 != 0) + return std::nullopt; + Value = overBits(VBinOp::BitOr, Bits, [&](unsigned K) { + return power(Width - 8 * (K / 8 + 1) + K % 8); + }); + break; + } + Value->BeginLoc = CE->getBeginLoc(); + Value->EndLoc = CE->getEndLoc(); + // GCC leaves the count of the bits of 0 undefined; a spec is total. + if ((Op != Clz && Op != Ctz) || + (CurrentFn && CurrentFn->IsSpec && !CurrentFn->IsConstexprSpec)) + return Value; + auto NonZero = std::make_unique( + VBinOp::Ne, cloneVExpr(Arg.get()), literal("0", Bits), VType::makeBool(), + Loc); + auto Require = std::make_unique( + std::move(NonZero), + static_cast(ProofObligationKind::BuiltinArgument), Loc); + Require->BeginLoc = CE->getBeginLoc(); + Require->EndLoc = CE->getEndLoc(); + auto Copy = cloneVExpr(Value.get()); + auto Guarded = std::make_unique( + std::move(Require), std::move(Value), std::move(Copy), Result, Loc); + Guarded->BeginLoc = CE->getBeginLoc(); + Guarded->EndLoc = CE->getEndLoc(); + return Guarded; +} + std::unique_ptr ASTConverter::convertConstexprSpec(const FunctionDecl *FD) { llvm::SaveAndRestore Owner(ErrorFunction, functionIdentity(FD)); @@ -4523,6 +4930,11 @@ ASTConverter::convertArrowFieldAddress(const MemberExpr *M) { return nullptr; } +static constexpr const char *OrderOpen = + ": C++ leaves the order of these operands open, and a call or a write in " + "one may change what the other reads; make it a statement of its own " + "first"; + std::optional ASTConverter::subscriptPlace(const ArraySubscriptExpr *AS) { if (!AS) @@ -4534,13 +4946,12 @@ ASTConverter::subscriptPlace(const ArraySubscriptExpr *AS) { const bool BaseReads = !(isa(Base) && Base->getType()->isArrayType()) && isHeapSensitive(AS->getBase()); + const bool IndexReads = isHeapSensitive(AS->getIdx()); if ((containsModifyingCall(AS->getIdx()) && BaseReads) || - (containsModifyingCall(AS->getBase()) && - isHeapSensitive(AS->getIdx()))) { - error(CurrentFn->Name + - ": C++ leaves the order of these operands open, and a call in " - "one may write what the other reads; make the call in a statement " - "of its own first"); + (containsModifyingCall(AS->getBase()) && IndexReads) || + writesWhatReads(AS->getIdx(), AS->getBase(), BaseReads) || + writesWhatReads(AS->getBase(), AS->getIdx(), IndexReads)) { + error(CurrentFn->Name + OrderOpen); return std::nullopt; } } @@ -6433,6 +6844,8 @@ std::unique_ptr ASTConverter::convertExprImpl(const Expr *E) { machineOperand(std::move(Op), U->getSubExpr()->getType(), Ctx), Ty, E->getExprLoc()); } + if (U->isIncrementDecrementOp() && CallSink && !InContractExpression) + return hoistSideEffect(U); error(CurrentFn->Name + ": unsupported unary operator"); return nullptr; } @@ -6448,6 +6861,22 @@ std::unique_ptr ASTConverter::convertExprImpl(const Expr *E) { Place->takeAccessCondition()); } if (const auto *B = dyn_cast(E)) { + if (B->isAssignmentOp() && CallSink && !InContractExpression) + return hoistSideEffect(B); + // A comma's left operand is evaluated first, once, its value discarded. + if (B->getOpcode() == BO_Comma && CallSink && !InContractExpression) { + if (!HoistedValues.count(B)) { + const size_t ErrorCount = Errors.size(); + std::vector> Discarded = + convertStmt(B->getLHS()); + if (Errors.size() != ErrorCount) + return nullptr; + for (auto &S : Discarded) + CallSink->push_back(std::move(S)); + HoistedValues[B] = {}; + } + return convertExpr(B->getRHS()); + } std::optional Op = convertBinOpcode(B->getOpcode()); if (!Op) { error(CurrentFn->Name + ": unsupported binary operator"); @@ -6458,10 +6887,7 @@ std::unique_ptr ASTConverter::convertExprImpl(const Expr *E) { // The operands are unsequenced: any order must give the same values. if (CallSink && !B->isLogicalOp() && orderDependent(B->getLHS(), B->getRHS())) { - error(CurrentFn->Name + - ": C++ leaves the order of these operands open, and a call in " - "one may write what the other reads; make the call in a statement " - "of its own first"); + error(CurrentFn->Name + OrderOpen); return nullptr; } if (IntMode == VIntMode::Math && @@ -6851,6 +7277,10 @@ std::unique_ptr ASTConverter::convertExprImpl(const Expr *E) { if (CE->getBuiltinCallee() == Builtin::BI__builtin_expect || CE->getBuiltinCallee() == Builtin::BI__builtin_expect_with_probability) return convertExpr(CE->getArg(0)); + if (auto Builtin = convertBitBuiltin(CE)) + return std::move(*Builtin); + if (auto Absolute = convertAbs(CE)) + return std::move(*Absolute); if (const FunctionDecl *Callee = CE->getDirectCallee()) { if (Callee->isConstexpr() && !functionContract(Callee) && CE->isEvaluatable(Ctx)) { @@ -6931,6 +7361,29 @@ std::unique_ptr ASTConverter::convertExprImpl(const Expr *E) { return nullptr; return hoistExecCall(CE, Callee); } + if (CallSink && !InContractExpression && !InGhost && !CurrentFn->IsSpec && + !CurrentFn->IsProof) { + const VType Ty = VType::fromQualType(E->getType(), IntMode, Ctx); + if (auto Hoisted = HoistedValues.find(CE); + Hoisted != HoistedValues.end()) + return std::make_unique( + Hoisted->second.first, Hoisted->second.second, E->getExprLoc()); + const std::string Temporary = + "__call_" + std::to_string(++NestedCallId); + if (auto Model = convertLibraryCall(CE, *CallSink, Temporary)) { + if (!*Model) + return nullptr; + auto Value = convertCallResultValue( + Temporary, (*Model)->getReturnType(), Ty, E->getExprLoc()); + if (!Value) + return nullptr; + const std::string Read = "__value_" + std::to_string(++NestedCallId); + CallSink->push_back(std::make_unique( + Read, std::move(Value), E->getExprLoc())); + HoistedValues[CE] = {Read, Ty}; + return std::make_unique(Read, Ty, E->getExprLoc()); + } + } if (functionContract(Callee)) error(CurrentFn->Name + ": executable call is unsupported in this expression " @@ -7087,8 +7540,8 @@ void ASTConverter::convertExecCallArgs( if (orderDependent(CE->getArg(I), CE->getArg(J))) { error(CurrentFn->Name + ": C++ leaves the order of these call arguments open, and a " - "call in one may write what another reads; make the call in a " - "statement of its own first"); + "call or a write in one may change what another reads; make it " + "a statement of its own first"); return; } @@ -7211,9 +7664,105 @@ bool ASTConverter::isHeapSensitive(const Stmt *S) const { S->children(), [&](const Stmt *Child) { return isHeapSensitive(Child); }); } +void ASTConverter::collectWrites(const Stmt *S, + std::set &Written, + bool &Memory) const { + if (!S) + return; + const Expr *Target = nullptr; + if (const auto *U = dyn_cast(S); + U && U->isIncrementDecrementOp()) + Target = U->getSubExpr(); + else if (const auto *B = dyn_cast(S); + B && B->isAssignmentOp()) + Target = B->getLHS(); + if (Target) { + // A field of a record held by value is part of the record's variable. + const Expr *Root = Target->IgnoreParenImpCasts(); + while (const auto *Member = dyn_cast(Root)) { + if (Member->isArrow()) + break; + Root = Member->getBase()->IgnoreParenImpCasts(); + } + const auto *Ref = dyn_cast(Root); + const auto *VD = Ref ? dyn_cast(Ref->getDecl()) : nullptr; + if (VD && !VD->getType()->isReferenceType() && !AddressableLocals.count(VD)) + Written.insert(VD); + else + Memory = true; + } + for (const Stmt *Child : S->children()) + collectWrites(Child, Written, Memory); +} + +static bool mentionsAny(const Stmt *S, + const std::set &Written) { + if (!S || Written.empty()) + return false; + if (const auto *Ref = dyn_cast(S)) + if (const auto *VD = dyn_cast(Ref->getDecl()); + VD && Written.count(VD)) + return true; + return llvm::any_of(S->children(), [&](const Stmt *Child) { + return mentionsAny(Child, Written); + }); +} + +bool ASTConverter::writesWhatReads(const Expr *Writer, const Expr *Reader, + bool ReaderReadsMemory) const { + std::set Written; + bool Memory = false; + collectWrites(Writer, Written, Memory); + return mentionsAny(Reader, Written) || (Memory && ReaderReadsMemory); +} + bool ASTConverter::orderDependent(const Expr *A, const Expr *B) const { return (containsModifyingCall(A) && isHeapSensitive(B)) || - (containsModifyingCall(B) && isHeapSensitive(A)); + (containsModifyingCall(B) && isHeapSensitive(A)) || + writesWhatReads(A, B, isHeapSensitive(B)) || + writesWhatReads(B, A, isHeapSensitive(A)); +} + +std::unique_ptr ASTConverter::hoistSideEffect(const Expr *E) { + const SourceLocation Loc = E->getExprLoc(); + if (auto Hoisted = HoistedValues.find(E); Hoisted != HoistedValues.end()) + return std::make_unique(Hoisted->second.first, + Hoisted->second.second, Loc); + const auto *U = dyn_cast(E); + const Expr *Target = U ? U->getSubExpr() : cast(E)->getLHS(); + if (Target->getType()->isPointerType() && isDynamicAddress(Target)) { + error(CurrentFn->Name + ": the value of an assignment, an increment, or a " + "decrement of a pointer to dynamic storage is " + "unsupported"); + return nullptr; + } + // The value is read where the expression is evaluated: a postfix + // operator's before its write, any other's after it. + const std::string Temporary = "__value_" + std::to_string(++NestedCallId); + VType Ty; + auto Read = [&] { + auto Value = convertExpr(Target); + if (!Value) + return false; + Ty = Value->Ty; + CallSink->push_back( + std::make_unique(Temporary, std::move(Value), Loc)); + return true; + }; + const bool Postfix = U && U->isPostfix(); + if (Postfix && !Read()) + return nullptr; + const size_t ErrorCount = Errors.size(); + ContinuesEvaluation = true; + std::vector> Effect = convertStmtBody(E); + if (Errors.size() != ErrorCount) + return nullptr; + for (auto &S : Effect) + CallSink->push_back(std::move(S)); + if (!Postfix && !Read()) + return nullptr; + HoistedValues[E] = {Temporary, Ty}; + return std::make_unique(Temporary, Ty, Loc); } bool ASTConverter::locatingIsHeapSensitive(const Expr *E) const { @@ -7239,9 +7788,10 @@ bool ASTConverter::locatingIsHeapSensitive(const Expr *E) const { std::unique_ptr ASTConverter::hoistExecCall(const CallExpr *CE, const FunctionDecl *Callee) { const VType Result = VType::fromQualType(CE->getType(), IntMode, Ctx); - if (auto Hoisted = HoistedCalls.find(CE); Hoisted != HoistedCalls.end()) - return convertCallResultValue(Hoisted->second, Callee->getReturnType(), - Result, CE->getExprLoc()); + if (auto Hoisted = HoistedValues.find(CE); Hoisted != HoistedValues.end()) + return convertCallResultValue(Hoisted->second.first, + Callee->getReturnType(), Result, + CE->getExprLoc()); const QualType Returned = Callee->getReturnType(); if (Returned->isVoidType() || Returned->isReferenceType() || Returned->isRecordType()) { @@ -7259,7 +7809,7 @@ std::unique_ptr ASTConverter::hoistExecCall(const CallExpr *CE, CallSink->push_back(atCall(std::make_unique( functionName(Callee), functionIdentity(Callee), std::move(Args), Temporary, CE->getExprLoc(), false), CE)); - HoistedCalls[CE] = Temporary; + HoistedValues[CE] = {Temporary, Result}; return convertCallResultValue(std::move(Temporary), Returned, Result, CE->getExprLoc()); } @@ -7438,8 +7988,13 @@ ASTConverter::convertAssignmentValue(const BinaryOperator *Assignment) { auto RHS = convertExpr(Assignment->getRHS()); if (!RHS) return nullptr; - // The right operand is evaluated before the left one, whose calls follow. - if (CallSink && containsExecCall(Assignment->getLHS())) { + // The right operand is evaluated before the left one, whose calls and + // writes follow. + std::set Written; + bool WritesMemory = false; + collectWrites(Assignment->getLHS(), Written, WritesMemory); + if (CallSink && (containsExecCall(Assignment->getLHS()) || !Written.empty() || + WritesMemory)) { const SourceLocation Loc = Assignment->getRHS()->getExprLoc(); const std::string Value = "__value_" + std::to_string(++NestedCallId); const VType Ty = RHS->Ty; @@ -8857,6 +9412,7 @@ void ASTConverter::appendReturn(std::unique_ptr Value, std::vector> ASTConverter::convertStmtBody(const Stmt *S) { + const bool Continues = std::exchange(ContinuesEvaluation, false); std::vector> Out; if (!S) return Out; @@ -8885,8 +9441,11 @@ ASTConverter::convertStmtBody(const Stmt *S) { CallSink, (isa(S) || isa(S)) && Executable ? &Out : nullptr); - llvm::SaveAndRestore Hoisted(HoistedCalls, - std::map()); + // A statement that continues an expression's evaluation keeps the values + // it has hoisted, and adds its own. + std::optional> Hoisted; + if (!Continues) + Hoisted.emplace(HoistedValues, decltype(HoistedValues)()); if (S->getStmtClass() == Stmt::ReturnStmtClass) { if (InGhost) { error(CurrentFn->Name + @@ -9461,6 +10020,8 @@ ASTConverter::convertStmtBody(const Stmt *S) { error(CurrentFn->Name + ": bare spec-call statement is unsupported"); return Out; } + if (convertLibraryCall(CE, Out, "")) + return Out; if (functionContract(Callee)) { std::vector> Args; convertExecCallArgs(CE, Out, Args); @@ -9681,13 +10242,15 @@ ASTConverter::convertStmtBody(const Stmt *S) { const bool TargetReads = BO->getOpcode() == BO_Assign ? locatingIsHeapSensitive(BO->getLHS()) : isHeapSensitive(BO->getLHS()); + const bool ValueReads = isHeapSensitive(BO->getRHS()); if ((containsModifyingCall(BO->getRHS()) && TargetReads) || - (containsModifyingCall(BO->getLHS()) && - isHeapSensitive(BO->getRHS()))) { + (containsModifyingCall(BO->getLHS()) && ValueReads) || + writesWhatReads(BO->getRHS(), BO->getLHS(), TargetReads) || + writesWhatReads(BO->getLHS(), BO->getRHS(), ValueReads)) { error(CurrentFn->Name + ": before C++17 the order of an assignment's operands is " - "open, and a call in one may write what the other reads; " - "make the call in a statement of its own first"); + "open, and a call or a write in one may change what the " + "other reads; make it a statement of its own first"); return Out; } } diff --git a/clang/lib/Verify/Frontend/ASTConverter.h b/clang/lib/Verify/Frontend/ASTConverter.h index a419726b4d..398b068a9f 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.h +++ b/clang/lib/Verify/Frontend/ASTConverter.h @@ -42,12 +42,16 @@ class ASTConverter { std::vector> *SubobjectSink = nullptr; unsigned SubobjectPointerId = 0; /// Where the statement or condition being lowered in executable code puts - /// the calls its expressions make, each into a temporary, in evaluation - /// order; null where no executable call can be made. + /// the calls and writes its expressions make, each value into a temporary, + /// in evaluation order; null where no executable call can be made. std::vector> *CallSink = nullptr; - /// The temporary of each call already put there, so converting an - /// expression twice calls once. - std::map HoistedCalls; + /// The temporary of each call, increment, decrement, or assignment already + /// put there, and its type, and each comma whose first operand is (with no + /// temporary), so converting an expression twice evaluates it once. + std::map> HoistedValues; + /// The next statement converted is a write an expression makes, which + /// continues its evaluation and keeps HoistedValues. + bool ContinuesEvaluation = false; std::vector Errors; /// The innermost declaration, statement, or expression being converted, /// where an error is reported unless it names a place of its own. @@ -235,6 +239,26 @@ class ASTConverter { /// std::max(a, b), or std::min(a, b), of two integers, as the standard /// defines it. std::unique_ptr convertMinOrMax(const CallExpr *CE, bool IsMax); + /// A call of a bit-counting or byte-swapping builtin, by its definition; + /// nullopt for any other call. + std::optional> convertBitBuiltin(const CallExpr *CE); + /// The models of (cppverify::model) that converted calls + /// use, in the order of their first use. + std::vector UsedLibraryModels; + /// The model named \p Name whose first parameter points to \p Element. + const FunctionDecl *libraryModel(llvm::StringRef Name, + QualType Element) const; + /// A call of memcpy, memmove, memset, or memcmp: a call of its model for + /// the objects its pointers address, into \p Out, with its result in + /// \p Result unless that is empty; the model, or null after an error. + /// Nothing for any other call. + std::optional + convertLibraryCall(const CallExpr *CE, + std::vector> &Out, + const std::string &Result); + /// abs, labs, llabs, and std::abs of an integer: its definition, in the + /// parameter's type (mathematical in a spec); nothing for any other call. + std::optional> convertAbs(const CallExpr *CE); void noteSpecUse(const FunctionDecl *FD); std::unique_ptr convertExpr(const Expr *E); std::unique_ptr convertExprImpl(const Expr *E); @@ -403,6 +427,19 @@ class ASTConverter { /// in the call sink, and a read of the temporary. std::unique_ptr hoistExecCall(const CallExpr *CE, const FunctionDecl *Callee); + /// An increment, a decrement, or an assignment whose value an expression + /// uses: its statements in the call sink, and a read of the value it has, + /// the old one for a postfix operator, in a temporary. + std::unique_ptr hoistSideEffect(const Expr *E); + /// The variables that the increments, decrements, and assignments in \p S + /// write (a field of a record held by value as its record's), and whether + /// one writes memory. + void collectWrites(const Stmt *S, std::set &Written, + bool &Memory) const; + /// Whether an increment, a decrement, or an assignment in \p Writer writes + /// a variable \p Reader names, or memory when \p ReaderReadsMemory. + bool writesWhatReads(const Expr *Writer, const Expr *Reader, + bool ReaderReadsMemory) const; /// A call of a contracted executable function, which may be hoisted. bool isExecCall(const Stmt *S) const; bool containsExecCall(const Stmt *S) const; diff --git a/clang/lib/Verify/IR/VStmt.cpp b/clang/lib/Verify/IR/VStmt.cpp index 477c700937..f6cff856d4 100644 --- a/clang/lib/Verify/IR/VStmt.cpp +++ b/clang/lib/Verify/IR/VStmt.cpp @@ -93,7 +93,7 @@ std::unique_ptr verify::cloneVStmt(const VStmt *S) { case VStmt::Assert: { const auto &A = static_cast(*S); return std::make_unique(cloneVExpr(A.Cond.get()), A.Loc, - A.ProofKind); + A.ProofKind, A.Note); } case VStmt::Assume: { const auto &A = static_cast(*S); diff --git a/clang/lib/Verify/IR/VStmt.h b/clang/lib/Verify/IR/VStmt.h index e57f0ca063..4ec53cc1bc 100644 --- a/clang/lib/Verify/IR/VStmt.h +++ b/clang/lib/Verify/IR/VStmt.h @@ -39,6 +39,7 @@ enum class ProofObligationKind { Deallocation, MissingReturn, Unreachable, + BuiltinArgument, Unsupported }; @@ -161,9 +162,12 @@ cloneMemoryChecks(const std::vector &Checks); struct VAssertStmt : VStmt { std::unique_ptr Cond; ProofObligationKind ProofKind; + /// For an unsupported obligation: what the verifier does not model here. + std::string Note; VAssertStmt(std::unique_ptr C, SourceLocation Loc, - ProofObligationKind ProofKind) - : VStmt(Assert, Loc), Cond(std::move(C)), ProofKind(ProofKind) {} + ProofObligationKind ProofKind, std::string Note = "") + : VStmt(Assert, Loc), Cond(std::move(C)), ProofKind(ProofKind), + Note(std::move(Note)) {} }; struct VAssumeStmt : VStmt { diff --git a/clang/lib/Verify/Transform/Passivize.cpp b/clang/lib/Verify/Transform/Passivize.cpp index d6ebe1e5cd..7560943584 100644 --- a/clang/lib/Verify/Transform/Passivize.cpp +++ b/clang/lib/Verify/Transform/Passivize.cpp @@ -4236,11 +4236,46 @@ class PassivizerImpl { return true; } - /// The element offset c of a slice actual `base + S*c` that a quantifier - /// indexes as `(base + S*c) + S*j`. - static const VExpr *sliceOffset(const VExpr *E, const std::string &Binder) { - if (!E) - return nullptr; + /// Whether two offsets are the same term, by structure. + static bool sameOffset(const VExpr *A, const VExpr *B) { + if (!A || !B || A->K != B->K) + return false; + switch (A->K) { + case VExpr::Literal: + return static_cast(A)->Value == + static_cast(B)->Value; + case VExpr::Var: + return static_cast(A)->Name == + static_cast(B)->Name; + case VExpr::Cast: + return sameRepresentation(A->Ty, B->Ty) && + sameOffset(static_cast(A)->Inner.get(), + static_cast(B)->Inner.get()); + case VExpr::BinOp: { + const auto *L = static_cast(A); + const auto *R = static_cast(B); + return L->Op == R->Op && sameOffset(L->Lhs.get(), R->Lhs.get()) && + sameOffset(L->Rhs.get(), R->Rhs.get()); + } + default: + return false; + } + } + + /// How a quantifier's loads use its binder j: the distinct element offsets + /// c of the slice actuals `base + S*c` it indexes as `(base + S*c) + S*j`, + /// whether one is indexed directly (`base + S*j`), and whether one uses j + /// otherwise. + struct SliceUse { + std::vector Offsets; + bool Direct = false; + bool Other = false; + }; + + static void collectSliceOffsets(const VExpr *E, const std::string &Binder, + SliceUse &Use) { + if (!E || Use.Other) + return; auto scaled = [](const VExpr *Term, uint64_t &Stride) -> const VExpr * { if (Term->K == VExpr::BinOp) { const auto *M = static_cast(Term); @@ -4255,27 +4290,41 @@ class PassivizerImpl { }; if (E->K == VExpr::Load) { const VExpr *Address = static_cast(E)->Ptr.get(); - if (Address->K == VExpr::BinOp) { - const auto *Outer = static_cast(Address); - if (Outer->Op == VBinOp::Add && Outer->Lhs->Ty.Kind == VTypeKind::Ptr && - Outer->Lhs->K == VExpr::BinOp) { - const auto *Inner = static_cast(Outer->Lhs.get()); - uint64_t IndexStride = 0, OffsetStride = 0; - const VExpr *Index = scaled(Outer->Rhs.get(), IndexStride); - if (Inner->Op == VBinOp::Add && - Inner->Lhs->Ty.Kind == VTypeKind::Ptr && Index->K == VExpr::Var && - static_cast(Index)->Name == Binder) { - const VExpr *Offset = scaled(Inner->Rhs.get(), OffsetStride); - if (OffsetStride == IndexStride && Offset->Ty.isInt()) - return Offset; - } + if (mentionsFree(Address, Binder)) { + const auto *Outer = Address->K == VExpr::BinOp + ? static_cast(Address) + : nullptr; + uint64_t IndexStride = 0, OffsetStride = 0; + const VExpr *Index = Outer && Outer->Op == VBinOp::Add + ? scaled(Outer->Rhs.get(), IndexStride) + : nullptr; + if (!Index || Outer->Lhs->Ty.Kind != VTypeKind::Ptr || + Index->K != VExpr::Var || + static_cast(Index)->Name != Binder || + mentionsFree(Outer->Lhs.get(), Binder)) { + Use.Other = true; + return; + } + const auto *Inner = + Outer->Lhs->K == VExpr::BinOp + ? static_cast(Outer->Lhs.get()) + : nullptr; + const VExpr *Offset = Inner && Inner->Op == VBinOp::Add && + Inner->Lhs->Ty.Kind == VTypeKind::Ptr + ? scaled(Inner->Rhs.get(), OffsetStride) + : nullptr; + if (Offset && OffsetStride == IndexStride && Offset->Ty.isInt()) { + if (llvm::none_of(Use.Offsets, [&](const VExpr *Seen) { + return sameOffset(Seen, Offset); + })) + Use.Offsets.push_back(Offset); + } else { + Use.Direct = true; } } } - const VExpr *Found = nullptr; auto visit = [&](const VExpr *Child) { - if (!Found) - Found = sliceOffset(Child, Binder); + collectSliceOffsets(Child, Binder, Use); }; switch (E->K) { case VExpr::BinOp: @@ -4302,68 +4351,110 @@ class PassivizerImpl { default: break; } - return Found; + } + + /// \p Q restated over the indices of a slice's base: j := k - c, a change + /// of variables. + std::unique_ptr rebased(const VQuantifiedExpr &Q, const VExpr *Offset, + const std::string &Name) { + const SourceLocation Loc = Q.Loc; + const VType MathTy = Q.BinderType; + auto mathOf = [&](const VExpr *V) -> std::unique_ptr { + if (V->Ty.IntMode == VIntMode::Math) + return cloneVExpr(V); + VType To = V->Ty; + To.IntMode = VIntMode::Math; + return std::make_unique(cloneVExpr(V), V->Ty, To, Loc); + }; + std::map> Shift; + Shift[Q.Binder] = std::make_unique( + VBinOp::Sub, std::make_unique(Name, MathTy, Loc), + mathOf(Offset), MathTy, Loc); + auto Body = substParamsInExpr(Q.Body.get(), Shift); + if (!Body) + return nullptr; + // Over all integers the shift changes no range. + std::unique_ptr Lo, Hi; + if (Q.Lo) { + Lo = std::make_unique(VBinOp::Add, mathOf(Q.Lo.get()), + mathOf(Offset), MathTy, Loc); + Hi = std::make_unique(VBinOp::Add, mathOf(Q.Hi.get()), + mathOf(Offset), MathTy, Loc); + } + if (Q.K == VExpr::Forall) + return std::make_unique(Name, std::move(Lo), std::move(Hi), + std::move(Body), Loc, MathTy); + return std::make_unique(Name, std::move(Lo), std::move(Hi), + std::move(Body), Loc, MathTy); } /// A contract quantifier that indexes a slice actual `base + c` from zero - /// is restated over base's indices: j := k - c is a change of variables, - /// and it lets the caller's own terms trigger the instantiation. - std::unique_ptr rebaseSliceBinders(std::unique_ptr E) { + /// is restated over base's indices, j := k - c, so that the caller's own + /// terms trigger its instantiation. With loads through slices at several + /// offsets, or directly, no one change of variables suits them all: an + /// assumption (\p Assumed) then keeps the quantifier and adds its + /// restatement over each slice's base, which are equivalent, each with the + /// triggers of its own form; a check is left as it is. + std::unique_ptr rebaseSliceBinders(std::unique_ptr E, + bool Assumed) { if (!E) return E; switch (E->K) { case VExpr::BinOp: { auto *B = static_cast(E.get()); - B->Lhs = rebaseSliceBinders(std::move(B->Lhs)); - B->Rhs = rebaseSliceBinders(std::move(B->Rhs)); + B->Lhs = rebaseSliceBinders(std::move(B->Lhs), Assumed); + B->Rhs = rebaseSliceBinders(std::move(B->Rhs), Assumed); return E; } case VExpr::UnaryOp: { auto *U = static_cast(E.get()); - U->Operand = rebaseSliceBinders(std::move(U->Operand)); + U->Operand = rebaseSliceBinders(std::move(U->Operand), Assumed); + return E; + } + case VExpr::Cast: { + auto *C = static_cast(E.get()); + C->Inner = rebaseSliceBinders(std::move(C->Inner), Assumed); + return E; + } + case VExpr::Conditional: { + auto *C = static_cast(E.get()); + C->Cond = rebaseSliceBinders(std::move(C->Cond), Assumed); + C->Then = rebaseSliceBinders(std::move(C->Then), Assumed); + C->Else = rebaseSliceBinders(std::move(C->Else), Assumed); return E; } case VExpr::Forall: case VExpr::Exists: { auto *Q = static_cast(E.get()); - Q->Body = rebaseSliceBinders(std::move(Q->Body)); + Q->Body = rebaseSliceBinders(std::move(Q->Body), Assumed); if (Q->BinderType.IntMode != VIntMode::Math) return E; - const VExpr *Offset = sliceOffset(Q->Body.get(), Q->Binder); - if (!Offset) + SliceUse Use; + collectSliceOffsets(Q->Body.get(), Q->Binder, Use); + if (Use.Other || Use.Offsets.empty()) return E; - const SourceLocation Loc = Q->Loc; - const VType MathTy = Q->BinderType; - auto mathOf = [&](const VExpr *V) -> std::unique_ptr { - if (V->Ty.IntMode == VIntMode::Math) - return cloneVExpr(V); - VType To = V->Ty; - To.IntMode = VIntMode::Math; - return std::make_unique(cloneVExpr(V), V->Ty, To, Loc); - }; - const std::string Rebased = Q->Binder + "_rebased"; - std::map> Shift; - Shift[Q->Binder] = std::make_unique( - VBinOp::Sub, std::make_unique(Rebased, MathTy, Loc), - mathOf(Offset), MathTy, Loc); - auto Body = substParamsInExpr(Q->Body.get(), Shift); - // Over all integers the shift changes no range. - std::unique_ptr Lo, Hi; - if (Q->Lo) { - Lo = std::make_unique(VBinOp::Add, mathOf(Q->Lo.get()), - mathOf(Offset), MathTy, Loc); - Hi = std::make_unique(VBinOp::Add, mathOf(Q->Hi.get()), - mathOf(Offset), MathTy, Loc); + if (Use.Offsets.size() == 1 && !Use.Direct) { + auto Restated = + rebased(*Q, Use.Offsets.front(), Q->Binder + "_rebased"); + return Restated ? std::move(Restated) : std::move(E); } - if (!Body) + if (!Assumed) return E; - if (E->K == VExpr::Forall) - return std::make_unique(Rebased, std::move(Lo), - std::move(Hi), std::move(Body), - Loc, MathTy); - return std::make_unique(Rebased, std::move(Lo), - std::move(Hi), std::move(Body), Loc, - MathTy); + std::unique_ptr All = std::move(E); + const auto &Original = static_cast(*All); + std::vector> Restatements; + for (size_t I = 0; I != Use.Offsets.size(); ++I) + if (auto Restated = + rebased(Original, Use.Offsets[I], + Original.Binder + "_rebased" + + (I ? std::to_string(I + 1) : std::string()))) + Restatements.push_back(std::move(Restated)); + const SourceLocation Loc = All->Loc; + for (auto &Restated : Restatements) + All = std::make_unique(VBinOp::And, std::move(All), + std::move(Restated), + VType::makeBool(), Loc); + return All; } default: return E; @@ -4513,6 +4604,7 @@ class PassivizerImpl { case ProofObligationKind::Initialization: case ProofObligationKind::PointerDifference: case ProofObligationKind::PointerValidity: + case ProofObligationKind::BuiltinArgument: return true; default: return false; @@ -5346,13 +5438,11 @@ class PassivizerImpl { for (const SafetyCheck &Check : Checks) { if (Fn.TotalExpressions && isDefinedness(Check.Kind)) continue; - // Anchor at the clause; an unfolded helper's operators may lie in - // another file. - auto Cond = cloneExpr(Check.Cond.get(), PCtx); - Cond->Loc = Post->Loc; - Cond->BeginLoc = Post->BeginLoc; - Cond->EndLoc = Post->EndLoc; - P.ExitAsserts.push_back({Check.Kind, afterEarlier(std::move(Cond))}); + // Anchored at the clause, the operation being its focus; an unfolded + // helper's operators may lie in another file. + P.ExitAsserts.push_back( + {Check.Kind, afterEarlier(cloneExpr(Check.Cond.get(), PCtx)), "", + {Post->Loc, Post->BeginLoc, Post->EndLoc}}); } auto Clause = cloneVExpr(BoundPost.get()); EarlierPosts = EarlierPosts ? makeAnd(std::move(EarlierPosts), @@ -6105,7 +6195,7 @@ class PassivizerImpl { return referencesVar(Pre, Name); }))) BoundPre = abstractValidity(std::move(BoundPre), Renames); - BoundPre = rebaseSliceBinders(std::move(BoundPre)); + BoundPre = rebaseSliceBinders(std::move(BoundPre), /*Assumed=*/false); SafetyChecks Checks; collectSafety(Pre, &FnMap, &Callee->ValidExtents, &CalleePointerParams, Checks, Fn.ObjectModel); @@ -6367,7 +6457,8 @@ class PassivizerImpl { PS->K = PassiveStmt::Assume; PS->Origin = "call:" + Callee->Name; PS->Cond = rebaseSliceBinders(substParams(Post.get(), PostParamMap, Ctx, - EntryHeap, "", {}, &ParamMap)); + EntryHeap, "", {}, &ParamMap), + /*Assumed=*/true); P.Stmts.push_back(std::move(PS)); } if (Callee->IsTrusted && P.Stmts.size() > FirstPost) { @@ -6390,9 +6481,10 @@ class PassivizerImpl { auto PS = std::make_unique(); PS->K = PassiveStmt::Assume; PS->Origin = "call:" + Callee->Name; - PS->Cond = rebaseSliceBinders( - substParams(Check.Cond.get(), PostParamMap, Ctx, EntryHeap, "", - {}, &ParamMap)); + PS->Cond = + rebaseSliceBinders(substParams(Check.Cond.get(), PostParamMap, + Ctx, EntryHeap, "", {}, &ParamMap), + /*Assumed=*/true); P.Stmts.push_back(std::move(PS)); } } @@ -7416,7 +7508,7 @@ class PassivizerImpl { A.ProofKind == ProofObligationKind::Initialization)) Cond = abstractValidity(std::move(Cond), Renames); emitPassive(P, PassiveStmt::Assert, std::move(Cond), Active.get(), A.Loc, - A.ProofKind); + A.ProofKind, A.Note); break; } case VStmt::Assume: { diff --git a/clang/lib/Verify/Transform/Passivize.h b/clang/lib/Verify/Transform/Passivize.h index 721ab03a84..afdd8eb37b 100644 --- a/clang/lib/Verify/Transform/Passivize.h +++ b/clang/lib/Verify/Transform/Passivize.h @@ -49,6 +49,9 @@ struct PassiveExitAssert { std::unique_ptr Cond; /// What an unsupported obligation stands for. std::string Note = {}; + /// Where the check is reported and identified, when that is not its + /// condition: the clause, for a check that the clause is defined. + SourceSpan Anchor = {}; }; enum class PassiveTraceKind { diff --git a/clang/test/Verify/suite/Inputs/global_abs.h b/clang/test/Verify/suite/Inputs/global_abs.h new file mode 100644 index 0000000000..6fab52b422 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/global_abs.h @@ -0,0 +1,10 @@ +// The overloads of abs that libc++'s defines in the global +// namespace, and the using-declaration of its . +#pragma clang system_header + +inline long abs(long x) noexcept { return __builtin_labs(x); } +inline long long abs(long long x) noexcept { return __builtin_llabs(x); } + +namespace std { +using ::abs; +} diff --git a/clang/test/Verify/suite/bit_builtins.cpp b/clang/test/Verify/suite/bit_builtins.cpp new file mode 100644 index 0000000000..b4ddf41086 --- /dev/null +++ b/clang/test/Verify/suite/bit_builtins.cpp @@ -0,0 +1,143 @@ +// RUN: not %cpp-verify --jobs=1 %s -- 2>&1 | FileCheck %s --check-prefixes=CHECK,BITS +// RUN: not %cpp-verify --jobs=1 --int-encoding=integer --function=l* \ +// RUN: --function=t* --function=c* --function=p* --function=f* --function=v* \ +// RUN: --function=spec_zero --function=asserts %s -- 2>&1 | FileCheck %s +// RUN: not %cpp-verify --jobs=1 --function=lz_zero --diagnostics-format=json %s -- 2>/dev/null | FileCheck %s --check-prefix=JSON +// +// GCC's bit-counting and byte-swapping builtins are their exact definitions +// over the operand's bits. __builtin_clz and __builtin_ctz of 0 are +// undefined: a builtin-argument check where the call is evaluated. In a spec, +// which is total, they count Width zeros there, as C++20's std::countl_zero. +// A static_assert with a message is a declaration with no effect. + +namespace cv = cppverify; + +int lz(unsigned x) + cv::pre(x != 0) + cv::post(0 <= cv::result && cv::result < 32) + cv::post(x >= 0x80000000u ? cv::result == 0 : cv::result > 0) +{ + return __builtin_clz(x); +} +// CHECK-DAG: Verified: lz [backend=z3] + +int lz_zero(unsigned x) + cv::post(cv::result >= 0) +{ + return __builtin_clz(x); +} +// CHECK-DAG: bit_builtins.cpp:[[@LINE-2]]:10: error: verification failed: lz_zero [builtin-argument] +// CHECK-DAG: bit_builtins.cpp:[[@LINE-3]]:10: note: counterexample: x = 0 +// JSON: "obligation":{"id":"{{.*}}::builtin-argument@[[#@LINE-4]]:3","kind":"builtin-argument","source":{"column":10,"end_column":26,"end_line":[[#@LINE-4]], + +int tz_zero(unsigned long long x) + cv::pre(x < 1000) + cv::post(cv::result >= 0) +{ + return x == 0 ? 64 : __builtin_ctzll(x) + __builtin_ctzll(x - x); +} +// CHECK-DAG: bit_builtins.cpp:[[@LINE-2]]:45: error: verification failed: tz_zero [builtin-argument] + +// The argument a contract gives a builtin must be one it is defined for: a +// verified body checks its postcondition where it returns. +int checked_contract(unsigned x) + cv::post(cv::result == __builtin_clz(x)) +{ + return __builtin_clz(x | 1u) + (x & 1u ? 0 : 0) - (x == 0 ? 0 : 0); +} +// CHECK-DAG: bit_builtins.cpp:[[@LINE-4]]:26: error: verification failed: checked_contract [builtin-argument] + +// A lifted helper's check is shown where the clause calls the helper. +constexpr int lz_of(unsigned v) { return __builtin_clz(v); } + +int lz_post(unsigned x) + cv::post(cv::result == lz_of(x)) +{ + return x == 0 ? 32 : __builtin_clz(x); +} +// CHECK-DAG: bit_builtins.cpp:[[@LINE-4]]:23: error: verification failed: lz_post [builtin-argument] + +int tz(unsigned long long x) + cv::pre(x != 0) + cv::post(0 <= cv::result && cv::result < 64) +{ + return __builtin_ctzll(x); +} +// CHECK-DAG: Verified: tz [backend=z3] + +int pop(unsigned x) + cv::post(0 <= cv::result && cv::result <= 32) + cv::post(x == 0 || cv::result > 0) +{ + return __builtin_popcount(x); +} +// CHECK-DAG: Verified: pop [backend=z3] + +int pop_wrong(unsigned x) + cv::post(cv::result < 32) +{ + return __builtin_popcount(x); +} +// CHECK-DAG: verification failed: pop_wrong [postcondition] +// CHECK-DAG: note: counterexample: x = 4294967295, result = 32 + +unsigned swap(unsigned x) + cv::post(cv::result == ((x & 0xffu) << 24 | (x & 0xff00u) << 8 | + (x >> 8 & 0xff00u) | x >> 24)) +{ + return __builtin_bswap32(x); +} +// The integer encoding gives each bitwise term an int2bv, and this +// comparison of 32 of them with shifts took longer than the test should. +// BITS-DAG: Verified: swap [backend=z3] + +int first(int x) + cv::post(x == 0 ? cv::result == 0 : 1 <= cv::result && cv::result <= 32) +{ + return __builtin_ffs(x); +} +// CHECK-DAG: Verified: first [backend=z3] + +int par(unsigned x) + cv::post(cv::result == __builtin_popcount(x) % 2) +{ + return __builtin_parity(x); +} +// CHECK-DAG: Verified: par [backend=z3] + +cv::spec int leading(unsigned x) { return __builtin_clz(x); } + +void spec_zero() + cv::post(true) +{ + cv::check(leading(0u) == 32); +} +// CHECK-DAG: Verified: spec_zero [backend=z3] + +// Each variant at the ends of its width and at a value of mixed bits. +void values() + cv::post(true) +{ + cv::check(__builtin_clz(1u) == 31 && __builtin_clz(0x80000000u) == 0); + cv::check(__builtin_clz(0x00f0f0f0u) == 8); + cv::check(__builtin_clzl(1ul) == 63 && __builtin_clzll(0x8000000000000000ull) == 0); + cv::check(__builtin_ctz(0x80000000u) == 31 && __builtin_ctz(0x00f0f0f0u) == 4); + cv::check(__builtin_ctzl(1ul) == 0 && __builtin_ctzll(0x8000000000000000ull) == 63); + cv::check(__builtin_popcount(0xffffffffu) == 32 && __builtin_popcount(0x00f0f0f0u) == 12); + cv::check(__builtin_popcountl(0ul) == 0 && __builtin_popcountll(0xf0f0f0f0f0f0f0f0ull) == 32); + cv::check(__builtin_parity(0x00f0f0f1u) == 1 && __builtin_parityll(3ull) == 0); + cv::check(__builtin_ffs(0) == 0 && __builtin_ffs(-2147483647 - 1) == 32); + cv::check(__builtin_ffsll(0x100ll) == 9 && __builtin_ffsl(1l) == 1); + cv::check(__builtin_bswap16((unsigned short)0x1234) == 0x3412); + cv::check(__builtin_bswap32(0x12345678u) == 0x78563412u); + cv::check(__builtin_bswap64(0x0102030405060708ull) == 0x0807060504030201ull); +} +// CHECK-DAG: Verified: values [backend=z3] + +int asserts(int x) + cv::post(cv::result == x) +{ + static_assert(sizeof(int) == 4, "int is 32 bits"); + return x; +} +// CHECK-DAG: Verified: asserts [backend=z3] diff --git a/clang/test/Verify/suite/contract_wellformedness.cpp b/clang/test/Verify/suite/contract_wellformedness.cpp index 03cb60247f..9db8cf8a82 100644 --- a/clang/test/Verify/suite/contract_wellformedness.cpp +++ b/clang/test/Verify/suite/contract_wellformedness.cpp @@ -180,7 +180,7 @@ int read_ahead(const int *p, int i) { return p[i]; } -// CHECK: [[@LINE-4]]:37: error: verification failed: read_ahead [bounds] +// CHECK: [[@LINE-4]]:40: error: verification failed: read_ahead [bounds] // BMC: error: verification failed: read_ahead [bounds] int one(int x) @@ -279,7 +279,7 @@ int next_object(const int *p, const int *q) p = p + 1; return q[0]; } -// CHECK: [[@LINE-5]]:37: error: verification failed: next_object [bounds] +// CHECK: [[@LINE-5]]:40: error: verification failed: next_object [bounds] int prev_object(const int *p, const int *q) cppverify::pre(valid(p, 2) && valid(q, 2) && q == p + 2 && p[2] == 0) diff --git a/clang/test/Verify/suite/dynamic_storage_fail.cpp b/clang/test/Verify/suite/dynamic_storage_fail.cpp index f15d51b2ac..6768339028 100644 --- a/clang/test/Verify/suite/dynamic_storage_fail.cpp +++ b/clang/test/Verify/suite/dynamic_storage_fail.cpp @@ -439,7 +439,7 @@ int modular_discarded_pointer_forwarding() // VERIFY-DAG: Unresolved: modular_copied_pointer_return {{.*}}[reason=construct.unsupported] // VERIFY-DAG: Unresolved: modular_unsafe_forwarding {{.*}}[reason=construct.unsupported] // VERIFY-DAG: Unresolved: modular_discarded_pointer_forwarding {{.*}}[reason=construct.unsupported] -// VERIFY-DAG: :107:37: error: verification failed: unsafe_forwarded_read [bounds] +// VERIFY-DAG: :107:55: error: verification failed: unsafe_forwarded_read [bounds] // VERIFY-DAG: Verified: modular_forwarded_scalar // VERIFY-DAG: Verified: modular_forwarded_temporary // VERIFY-DAG: Verified: modular_forwarded_control diff --git a/clang/test/Verify/suite/library_abs_global.cpp b/clang/test/Verify/suite/library_abs_global.cpp new file mode 100644 index 0000000000..92de974b68 --- /dev/null +++ b/clang/test/Verify/suite/library_abs_global.cpp @@ -0,0 +1,37 @@ +// RUN: %cpp-verify --jobs=1 %s -- 2>&1 | FileCheck %s +// RUN: not %cpp-verify --jobs=1 %s -- -DUSER_ABS 2>&1 | FileCheck %s --check-prefix=USER +// +// std::abs of a long is libc++'s global abs(long) from , brought +// into std by , where libstdc++ defines it in std itself: either is +// the absolute value. A global abs of the user's own is not. + +#ifndef USER_ABS +#include "Inputs/global_abs.h" + +long distance(long a, long b) + cppverify::pre(-1000000 <= a && a <= 1000000 && -1000000 <= b && b <= 1000000) + cppverify::post(cppverify::result == (a < b ? b - a : a - b)) +{ + return std::abs(a - b); +} +// CHECK: Verified: distance [backend=z3] + +long long magnitude(long long x) + cppverify::pre(x > -9223372036854775807LL) + cppverify::post(cppverify::result >= 0) +{ + return abs(x); +} +// CHECK: Verified: magnitude [backend=z3] +#else +// Not the absolute value: modeled as one, magnitude would verify. +long abs(long x) { return x; } + +long magnitude(long x) + cppverify::pre(x > -9223372036854775807L) + cppverify::post(cppverify::result >= 0) +{ + return abs(x); +} +// USER-NOT: Verified: magnitude +#endif diff --git a/clang/test/Verify/suite/library_models.cpp b/clang/test/Verify/suite/library_models.cpp new file mode 100644 index 0000000000..691e6b6547 --- /dev/null +++ b/clang/test/Verify/suite/library_models.cpp @@ -0,0 +1,240 @@ +// RUN: not %cpp-verify --jobs=1 %s -- > %t 2>&1 +// RUN: FileCheck %s < %t +// RUN: FileCheck %s --check-prefix=QUIET < %t +// +// memcpy, memmove, memset, and memcmp of integers are calls of their models +// in , which every proof that uses one trusts; abs is its +// definition, undefined at the minimum. A model is converted only where a +// call uses it, and is not reported. +// +// QUIET-NOT: Trusted: + +#include +#include + +namespace cv = cppverify; + +void copy(int *dst, const int *src, int n) + cv::pre(cv::valid(dst, n) && cv::valid(src, n) && 0 <= n && n <= 1000) + cv::modifies(dst[0 : n]) + cv::post(cv::forall(k, 0, n, dst[k] == src[k])) +{ + memcpy(dst, src, n * sizeof(int)); +} +// CHECK-DAG: Verified: copy [backend=z3] [trusts=memcpy] + +// A caller trusts what its callee's proof trusts. +void copy_twice(int *a, int *b, const int *c) + cv::pre(cv::valid(a, 4) && cv::valid(b, 4) && cv::valid(c, 4)) + cv::modifies(a[0 : 4], b[0 : 4]) + cv::post(a[3] == c[3] && b[3] == c[3]) +{ + copy(a, c, 4); + std::memcpy(b, a, sizeof(int) * 4); +} +// CHECK-DAG: Verified: copy_twice [backend=z3] [trusts=memcpy] + +void shift_left(int *a, int n) + cv::pre(cv::valid(a, n) && 1 <= n && n <= 1000) + cv::modifies(a[0 : n]) + cv::post(cv::forall(k, 0, n - 1, a[k] == cv::old(a[k + 1]))) +{ + memmove(a, a + 1, (n - 1) * sizeof(int)); +} +// CHECK-DAG: Verified: shift_left [backend=z3] [trusts=memmove] + +void shift_right(short *a, int n) + cv::pre(cv::valid(a, n) && 1 <= n && n <= 1000) + cv::modifies(a[0 : n]) + cv::post(cv::forall(k, 1, n, a[k] == cv::old(a[k - 1]))) +{ + memmove(a + 1, a, (n - 1) * sizeof(short)); +} +// CHECK-DAG: Verified: shift_right [backend=z3] [trusts=memmove] + +enum class Color : unsigned char { Red, Green, Blue }; + +void copy_colors(Color *dst, const Color *src) + cv::pre(cv::valid(dst, 3) && cv::valid(src, 3)) + cv::modifies(dst[0 : 3]) + cv::post(dst[2] == src[2]) +{ + memcpy(dst, src, 3); +} +// CHECK-DAG: Verified: copy_colors [backend=z3] [trusts=memcpy] + +void clear(unsigned *a, int n) + cv::pre(cv::valid(a, n) && 0 <= n && n <= 1000) + cv::modifies(a[0 : n]) + cv::post(cv::forall(k, 0, n, a[k] == 0)) +{ + memset(a, 0, n * sizeof(unsigned)); +} +// CHECK-DAG: Verified: clear [backend=z3] [trusts=memset] + +void ones(int *a, int n) + cv::pre(cv::valid(a, n) && 0 <= n && n <= 1000) + cv::modifies(a[0 : n]) + cv::post(cv::forall(k, 0, n, a[k] == -1)) +{ + memset(a, 0xff, n * sizeof(int)); +} +// CHECK-DAG: Verified: ones [backend=z3] [trusts=memset] + +void fill_bytes(unsigned char *a, int n, int c) + cv::pre(cv::valid(a, n) && 0 <= n && n <= 1000) + cv::modifies(a[0 : n]) + cv::post(cv::forall(k, 0, n, a[k] == (c & 255))) +{ + memset(a, c, n); +} +// CHECK-DAG: Verified: fill_bytes [backend=z3] [trusts=memset] + +// The byte is (unsigned char)-1, 0xff. +void minus_one(int *a, int n) + cv::pre(cv::valid(a, n) && 0 <= n && n <= 1000) + cv::modifies(a[0 : n]) + cv::post(cv::forall(k, 0, n, a[k] == -1)) +{ + memset(a, -1, n * sizeof(int)); +} +// CHECK-DAG: Verified: minus_one [backend=z3] [trusts=memset] + +// Each byte is 1, so each int is 0x01010101. +void wrong_fill(int *a) + cv::pre(cv::valid(a, 2)) + cv::modifies(a[0 : 2]) + cv::post(a[0] == 1) +{ + memset(a, 1, 2 * sizeof(int)); +} +// CHECK-DAG: verification failed: wrong_fill [postcondition] + +bool same(const int *a, const int *b, int n) + cv::pre(cv::valid(a, n) && cv::valid(b, n) && 0 <= n && n <= 1000) + cv::post(cv::result == cv::forall(k, 0, n, a[k] == b[k])) +{ + return memcmp(a, b, n * sizeof(int)) == 0; +} +// CHECK-DAG: Verified: same [backend=z3] [trusts=memcmp] + +int before(const unsigned char *a, const unsigned char *b, int n) + cv::pre(cv::valid(a, n) && cv::valid(b, n) && 1 <= n && n <= 1000) + cv::post(a[0] < b[0] ? cv::result < 0 : true) +{ + return memcmp(a, b, n); +} +// CHECK-DAG: Verified: before [backend=z3] [trusts=memcmp] + +void overlap(int *a, int n) + cv::pre(cv::valid(a, n) && 2 <= n && n <= 1000) + cv::modifies(a[0 : n]) + cv::post(true) +{ + memcpy(a, a + 1, (n - 1) * sizeof(int)); +} +// CHECK-DAG: library_models.cpp:[[@LINE-2]]:3: error: verification failed: overlap [aliasing] + +void past_end(int *dst, const int *src) + cv::pre(cv::valid(dst, 4) && cv::valid(src, 4)) + cv::modifies(dst[0 : 4]) + cv::post(true) +{ + memcpy(dst, src, 5 * sizeof(int)); +} +// CHECK-DAG: verification failed: past_end + +void part(int *dst, const int *src, int bytes) + cv::pre(cv::valid(dst, 4) && cv::valid(src, 4) && 0 <= bytes && bytes <= 16) + cv::modifies(dst[0 : 4]) + cv::post(true) +{ + memcpy(dst, src, bytes); +} +// CHECK-DAG: Unresolved: part [backend=z3] [reason=construct.unsupported] (the verifier cannot model a construct here: memcpy of a size that splits an object) + +void widen(int *dst, const short *src) + cv::pre(cv::valid(dst, 2) && cv::valid(src, 4)) + cv::modifies(dst[0 : 2]) + cv::post(true) +{ + memcpy(dst, src, 8); +} +// CHECK-DAG: error: widen: memcpy of 'int *' and 'const short *' is unsupported: it is modeled for pointers to integers of one size + +void flags(bool *dst, const char *src) + cv::pre(cv::valid(dst, 2) && cv::valid(src, 2)) + cv::modifies(dst[0 : 2]) + cv::post(true) +{ + memcpy(dst, src, 2); +} +// CHECK-DAG: error: flags: memcpy of 'bool *' and 'const char *' is unsupported: it is modeled for pointers to integers of one size + +int unsequenced_size(int *dst, const int *src, int i) + cv::pre(cv::valid(dst, 4) && cv::valid(src, 4) && 0 <= i && i < 2) + cv::modifies(dst[0 : 4]) + cv::post(true) +{ + memcpy(dst + i, src, i++ * sizeof(int)); + return i; +} +// CHECK-DAG: error: unsequenced_size: C++ leaves the order of these call arguments open, and a call or a write in one may change what another reads + +struct Pt { + int x; + int y; +}; + +void copy_point(Pt *dst, const Pt *src) + cv::pre(dst != nullptr && src != nullptr) + cv::modifies(*dst) + cv::post(true) +{ + memcpy(dst, src, sizeof(Pt)); +} +// CHECK-DAG: error: copy_point: memcpy of 'Pt *' and 'const Pt *' is unsupported: it is modeled for pointers to integers of one size + +int magnitude(int x) + cv::pre(x > -2147483647 - 1) + cv::post(cv::result >= 0 && (cv::result == x || cv::result == -x)) +{ + return abs(x); +} +// CHECK-DAG: Verified: magnitude [backend=z3] + +long distance(long a, long b) + cv::pre(-1000000 <= a && a <= 1000000 && -1000000 <= b && b <= 1000000) + cv::post(cv::result == (a < b ? b - a : a - b)) +{ + return std::abs(a - b); +} +// CHECK-DAG: Verified: distance [backend=z3] + +int any_magnitude(int x) + cv::post(cv::result >= 0) +{ + return abs(x); +} +// CHECK-DAG: library_models.cpp:[[@LINE-2]]:10: error: verification failed: any_magnitude [overflow] +// CHECK-DAG: note: counterexample: x = -2147483648 + +// In a spec, whose integers are mathematical, abs is the absolute value. +cv::spec long long magnitude_of(int x) { return abs(x); } + +void spec_magnitude() + cv::post(true) +{ + cv::check(magnitude_of(-2147483647 - 1) == 2147483648LL); +} +// CHECK-DAG: Verified: spec_magnitude [backend=z3] + +// In a contract abs is C++ too: undefined at the minimum. +int abs_contract(int x) + cv::post(cv::result == abs(x)) +{ + if (x == -2147483647 - 1) + return 0; + return x < 0 ? -x : x; +} +// CHECK-DAG: library_models.cpp:[[@LINE-6]]:26: error: verification failed: abs_contract [overflow] diff --git a/clang/test/Verify/suite/out_parameters.cpp b/clang/test/Verify/suite/out_parameters.cpp index 9ef1fa4d56..b581854c42 100644 --- a/clang/test/Verify/suite/out_parameters.cpp +++ b/clang/test/Verify/suite/out_parameters.cpp @@ -452,8 +452,8 @@ void set_if(int &x, bool c) if (c) x = 1; } -// CHECK: :[[@LINE-5]]:14: error: verification failed: set_if [initialization] -// NOUB: :[[@LINE-6]]:14: error: verification failed: set_if [initialization] +// CHECK: :[[@LINE-5]]:12: error: verification failed: set_if [initialization] +// NOUB: :[[@LINE-6]]:12: error: verification failed: set_if [initialization] // A loop writes on no path known before it runs. void zero_each(int &x, int n) diff --git a/clang/test/Verify/suite/side_effect_values.cpp b/clang/test/Verify/suite/side_effect_values.cpp new file mode 100644 index 0000000000..1dbbb5b834 --- /dev/null +++ b/clang/test/Verify/suite/side_effect_values.cpp @@ -0,0 +1,322 @@ +// RUN: not %cpp-verify --jobs=1 %s -- > %t 2>&1 +// RUN: FileCheck %s < %t +// RUN: FileCheck %s --check-prefix=SOUND < %t +// RUN: %cpp-verify --lower-only --dump-ir=1 --function=twice_once %s -- 2>&1 | FileCheck %s --check-prefix=VCR +// RUN: not %cpp-verify --jobs=1 %s -- -DORDER 2>&1 | FileCheck %s --check-prefix=ORDER +// RUN: not %cpp-verify --jobs=1 --function=old_index --function=new_index %s -- -std=c++14 2>&1 | FileCheck %s --check-prefix=CXX14 +// +// An increment, a decrement, an assignment, or a comma expression may stand +// where its value is used: its write runs where C++ evaluates it, and the +// value is read there, the old one for a postfix operator. C++ leaves the +// order of unsequenced operands open, so a write that another operand may +// read is an error. +// +// SOUND-NOT: vacuous + +namespace cv = cppverify; + +int post_inc(int x) + cv::pre(x < 100) + cv::post(cv::result == x) +{ + int y = x; + int z = y++; + cv::check(y == x + 1); + return z; +} +// CHECK-DAG: Verified: post_inc + +int pre_dec(int x) + cv::pre(x > -100) + cv::post(cv::result == x - 1) +{ + int y = x; + return --y; +} +// CHECK-DAG: Verified: pre_dec + +int chain() + cv::post(cv::result == 0) +{ + int a, b; + a = b = 0; + return a + b; +} +// CHECK-DAG: Verified: chain + +int compound_value(int x) + cv::pre(0 <= x && x < 100) + cv::post(cv::result == 2 * x + 3) +{ + int y = x; + int z = (y += 3) + x; + cv::check(y == x + 3); + return z; +} +// CHECK-DAG: Verified: compound_value + +int first_nonzero(const int *p, int n) + cv::pre(cv::valid(p, n) && n >= 1) + cv::post(cv::result == p[0] || (p[0] == 0 && cv::result == -1)) +{ + int c; + if ((c = p[0]) != 0) + return c; + return -1; +} +// CHECK-DAG: Verified: first_nonzero + +int sum(const int *a, int n) + cv::pre(cv::valid(a, n) && 0 <= n && n <= 100) + cv::pre(cv::forall(k, 0, n, 0 <= a[k] && a[k] <= 100)) + cv::post(0 <= cv::result && cv::result <= 100 * n) +{ + int s = 0; + int i = 0; + while (i < n) + cv::invariant(0 <= i && i <= n && 0 <= s && s <= 100 * i) + cv::decreases(n - i) + { + s = s + a[i++]; + } + return s; +} +// CHECK-DAG: Verified: sum + +void copy(int *dst, const int *src, int n) + cv::pre(cv::valid(dst, n) && cv::valid(src, n) && 0 <= n && n < 1000) + cv::modifies(dst[0 : n]) + cv::post(cv::forall(k, 0, n, dst[k] == src[k])) +{ + int *d = dst; + const int *s = src; + for (int i = 0; i < n; i = i + 1) + cv::invariant(0 <= i && i <= n && d == dst + i && s == src + i) + cv::invariant(cv::forall(k, 0, i, dst[k] == src[k])) + cv::decreases(n - i) + { + *d++ = *s++; + } +} +// CHECK-DAG: Verified: copy + +int countdown(int k) + cv::pre(0 <= k && k < 100) + cv::post(cv::result == 0) +{ + while (k-- > 0) + cv::invariant(0 <= k && k < 100) + cv::decreases(k) + { + } + return k + 1; +} +// CHECK-DAG: Verified: countdown + +int comma_value(int i, int j) + cv::pre(0 <= i && i < 100 && 0 <= j && j < 100) + cv::post(cv::result == i + j + 1) +{ + int a = i; + int b = j; + for (int k = 0; k < 1; k++, a++, b--) + cv::invariant(0 <= k && k <= 1 && a == i + k && b == j - k) + cv::decreases(1 - k) + { + } + return (a++, a + b); +} +// CHECK-DAG: Verified: comma_value + +int old_of_memory(int *p) + cv::pre(p != nullptr && *p < 1000) + cv::modifies(*p) + cv::post(cv::result == cv::old(*p) && *p == cv::old(*p) + 1) +{ + return (*p)++; +} +// CHECK-DAG: Verified: old_of_memory + +// The target of a compound assignment is read and written once: its increment +// runs once. +int twice_once(int *a, int i) + cv::pre(cv::valid(a, 4) && 0 <= i && i < 4 && a[i] < 1000) + cv::modifies(a[0 : 4]) + cv::post(a[i] == cv::old(a[i]) + 1 && cv::result == i + 1) +{ + a[i++] += 1; + return i; +} +// CHECK-DAG: Verified: twice_once +// VCR-LABEL: fn twice_once +// VCR: assign __value_[[ONE:[0-9]+]] +// VCR-NEXT: 1 +// VCR-NEXT: assign __value_[[K:[0-9]+]] +// VCR-NEXT: i +// VCR-NEXT: assign i +// VCR-NOT: assign i +// VCR: store +// VCR-NEXT: + +// VCR-NEXT: a +// VCR-NEXT: * +// VCR-NEXT: cast +// VCR-NEXT: __value_[[K]] +// VCR: load +// VCR: __value_[[K]] +// VCR: __value_[[ONE]] +// VCR-NEXT: return + +int nested_once(int *a, int i) + cv::pre(cv::valid(a, 4) && 0 <= i && i < 4 && a[i] < 1000) + cv::modifies(a[0 : 4]) + cv::post(cv::result == cv::old(a[i]) && a[i] == cv::old(a[i]) + 1) +{ + int k = i; + int v = a[k++]++; + cv::check(k == i + 1); + return v; +} +// CHECK-DAG: Verified: nested_once + +// A comma in such a target runs its first operand once. +int comma_target(int *a, int i) + cv::pre(cv::valid(a, 4) && 0 <= i && i < 3 && a[i + 1] < 1000) + cv::modifies(a[0 : 4]) + cv::post(a[i + 1] == cv::old(a[i + 1]) + 1 && cv::result == i + 1) +{ + int k = i; + a[(k++, k)] += 1; + return k; +} +// CHECK-DAG: Verified: comma_target + +// The value is read before the target is located (C++17). +void old_index(int *a, int i) + cv::pre(cv::valid(a, 4) && 0 <= i && i < 3) + cv::modifies(a[0 : 4]) + cv::post(a[i] == i) +{ + int k = i; + a[k++] = k; +} +// CHECK-DAG: Verified: old_index +// CXX14-DAG: error: old_index: before C++17 the order of an assignment's operands is open, and a call or a write in one may change what the other reads + +// The target is located after the value's write. +void new_index(int *a, int i) + cv::pre(cv::valid(a, 4) && 0 <= i && i < 3) + cv::modifies(a[0 : 4]) + cv::post(a[i + 1] == i) +{ + int k = i; + a[k] = k++; +} +// CHECK-DAG: Verified: new_index +// CXX14-DAG: error: new_index: before C++17 the order of an assignment's operands is open + +// A write on one path of a ?: or && runs on that path only. +int on_path(int x, bool c) + cv::pre(0 <= x && x < 100) + cv::post(cv::result == (c ? x + 1 : x)) +{ + int y = x; + int v = c ? y++ : 0; + int w = (c && (v = 1)) ? 0 : 0; + return y + w; +} +// CHECK-DAG: Verified: on_path + +int past_end(const int *a, int n) + cv::pre(cv::valid(a, n) && n == 1) + cv::post(true) +{ + int i = 0; + int v = a[i++]; + cv::check(v == a[0]); + return a[i++]; +} +// CHECK-DAG: side_effect_values.cpp:[[@LINE-2]]:10: error: verification failed: past_end [bounds] + +int wrong_old(int x) + cv::pre(x < 100) + cv::post(cv::result == x + 1) +{ + int y = x; + return y++; +} +// CHECK-DAG: side_effect_values.cpp:[[@LINE-5]]:23: error: verification failed: wrong_old [postcondition] + +#ifdef ORDER +int unsequenced(int i) + cv::pre(0 <= i && i < 100) + cv::post(true) +{ + return i++ + i; +} +// ORDER-DAG: error: unsequenced: C++ leaves the order of these operands open, and a call or a write in one may change what the other reads + +int read_twice(int i, int j) + cv::pre(0 <= i && i < 100) + cv::post(cv::result == j) +{ + return j; +} + +int arguments(int i) + cv::pre(0 <= i && i < 99) + cv::post(true) +{ + return read_twice(i++, i); +} +// ORDER-DAG: error: arguments: C++ leaves the order of these call arguments open, and a call or a write in one may change what another reads + +struct Buf { + int *data; +}; + +int index_write(Buf *b) + cv::pre(b != nullptr && cv::valid(b->data, 4)) + cv::modifies(b->data[0 : 4]) + cv::post(true) +{ + return b->data[b->data[0]++]; +} +// ORDER-DAG: error: index_write: C++ leaves the order of these operands open + +struct Pair { + int f; + int g; +}; + +int field_read(Pair s) + cv::pre(0 <= s.f && s.f < 100) + cv::post(true) +{ + return s.f++ + s.f; +} +// ORDER-DAG: error: field_read: C++ leaves the order of these operands open + +struct Counter { + int n; + + int bump() + cv::pre(0 <= n && n < 100) + cv::modifies(n) + cv::post(true) + { + return n++ + n; + } +}; +// ORDER-DAG: error: Counter::bump: C++ leaves the order of these operands open + +int dynamic_assign() + cv::post(true) +{ + int *q = new int(1); + int *p = nullptr; + if ((p = q) != nullptr) + delete q; + return 0; +} +// ORDER-DAG: error: dynamic_assign: the value of an assignment, an increment, or a decrement of a pointer to dynamic storage is unsupported +#endif diff --git a/clang/test/Verify/suite/slice_quantifier_offsets.cpp b/clang/test/Verify/suite/slice_quantifier_offsets.cpp new file mode 100644 index 0000000000..c73206a84e --- /dev/null +++ b/clang/test/Verify/suite/slice_quantifier_offsets.cpp @@ -0,0 +1,50 @@ +// RUN: %cpp-verify --jobs=1 --timeout=5000 %s -- 2>&1 | FileCheck %s +// RUN: %cpp-verify --lower-only --dump-ir=2 --function=shifted %s -- 2>&1 | FileCheck %s --check-prefix=MIXED +// RUN: %cpp-verify --lower-only --dump-ir=2 --function=both_shifted %s -- 2>&1 | FileCheck %s --check-prefix=SHARED +// +// A callee's quantifier over its parameters' elements is restated over a +// slice actual's base (j := k - c) when every element it reads goes through +// that one slice `base + c`, so that the caller's reads trigger it. When it +// also reads at another offset, no change of variables suits both: an assumed +// postcondition keeps the quantifier and adds its restatement over each +// slice's base, equivalent, and the caller's reads trigger one of them. + +namespace cv = cppverify; + +[[cppverify::trusted]] void copy(int *d, const int *s, long k) + cv::pre(cv::valid(d, k) && cv::valid(s, k)) + cv::modifies(d[0 : k]) + cv::post(cv::forall(i, 0, k, d[i] == cv::old(s[i]))); + +[[cppverify::trusted]] bool all_positive(const int *s, long k) + cv::pre(cv::valid(s, k)) + cv::post(cv::result == cv::forall(i, 0, k, s[i] > 0)); + +void shifted(int *a, const int *b, int n) + cv::pre(cv::valid(a, n) && cv::valid(b, n + 1) && 1 <= n && n <= 1000) + cv::modifies(a[0 : n]) + cv::post(cv::forall(k, 0, n, a[k] == b[k + 1])) +{ + copy(a, b + 1, n); +} +// CHECK-DAG: Verified: shifted [backend=z3] [trusts=copy] +// MIXED: forall __cppverify_bound_0_i{{$}} +// MIXED: forall __cppverify_bound_0_i_rebased{{$}} + +void shifted_target(int *a, const int *b, int n) + cv::pre(cv::valid(a, n + 1) && cv::valid(b, n) && 1 <= n && n <= 1000) + cv::modifies(a[0 : n + 1]) + cv::post(cv::forall(k, 1, n + 1, a[k] == b[k - 1])) +{ + copy(a + 1, b, n); +} +// CHECK-DAG: Verified: shifted_target [backend=z3] [trusts=copy] + +bool both_shifted(const int *b, int n) + cv::pre(cv::valid(b, n + 1) && 1 <= n && n <= 1000) + cv::post(cv::result == cv::forall(k, 1, n + 1, b[k] > 0)) +{ + return all_positive(b + 1, n); +} +// CHECK-DAG: Verified: both_shifted [backend=z3] [trusts=all_positive] +// SHARED: _rebased diff --git a/clang/utils/cppverify-differential/cases/library.py b/clang/utils/cppverify-differential/cases/library.py new file mode 100644 index 0000000000..7339adc626 --- /dev/null +++ b/clang/utils/cppverify-differential/cases/library.py @@ -0,0 +1,171 @@ +"""The C library's memcpy, memmove, memset, memcmp, and abs against their +models: each contract below is verified with the model's trust, so a run +that breaks it is a model the library does not conform to (UNSOUND), and the +false claims must not verify.""" +import random +from differential import * # noqa: F401,F403 + +R = 'cppverify::result' +O = 'cppverify::old' +FA = 'cppverify::forall' +V = 'cppverify::valid' +C = [] + + +def case(*a, **k): + C.append(PCase(*a, **k)) + + +def values(rng, n, t): + a, b = trange(t) + return [rng.choice([a, b, 0, 1, -1 if a < 0 else 0]) if rng.random() < 0.3 + else rng.randint(a, b) for _ in range(n)] + + +def two_buffers(t, count=200, seed=11, same=False): + def g(): + rng = random.Random(seed) + out = [] + for _ in range(count): + n = rng.randint(0, 8) + d = values(rng, n, t) + s = list(d) if same and rng.random() < 0.5 else values(rng, n, t) + if same and n and rng.random() < 0.3: + s[rng.randrange(n)] = d[rng.randrange(n)] + out.append({'n': n, 'd': d, 's': s}) + return out + return g + + +def one_buffer(t, count=200, seed=13, scalar=None): + def g(): + rng = random.Random(seed) + out = [] + for _ in range(count): + n = rng.randint(0, 8) + d = {'n': n, 'a': values(rng, n, t)} + if scalar: + d[scalar] = rng.choice([0, 1, 0xff, 0x80, 0x7f, -1, 256, 0x1234, + rng.randint(-2**31, 2**31 - 1)]) + out.append(d) + return out + return g + + +def repeated(c, t): + """The value of a t whose every byte is (unsigned char)c.""" + bits, _ = TYPES[t] + v = 0 + for _ in range(bits // 8): + v = (v << 8) | (c & 255) + return wrap(v, t) + + +def memset_value(t): + """The byte (unsigned char)c repeated in a t, in contract arithmetic.""" + bits, signed = TYPES[t] + value = '(c & 255) * %dULL' % sum(256 ** j for j in range(bits // 8)) + if signed: + whole = '2 * 9223372036854775808ULL' if bits == 64 else str(2 ** bits) + value = '(%s - ((c & 128) != 0 ? %s : 0))' % (value, whole) + return value + + +TYPES_UNDER_TEST = ['char', 'signed char', 'unsigned char', 'short', + 'unsigned short', 'int', 'unsigned', 'long', + 'unsigned long long'] + +for t in TYPES_UNDER_TEST: + tag = t.replace(' ', '_') + case('l_memcpy_' + tag, + [('b', t, 'd', 'n'), ('b', 'const ' + t, 's', 'n'), ('s', 'int', 'n')], 'void', + 'cppverify::pre(%s(d, n) && %s(s, n) && 0 <= n && n <= 1000)\n' + 'cppverify::modifies(d[0 : n])\n' + 'cppverify::post(%s(k, 0, n, d[k] == s[k]))' % (V, V, FA), + 'memcpy(d, s, n * sizeof(%s));' % t, inputs=two_buffers(t), + prelude='#include ', + post=lambda i, b, r: b[0] == i['s'] and b[1] == i['s']) + case('l_memset_' + tag, + [('b', t, 'a', 'n'), ('s', 'int', 'n'), ('s', 'int', 'c')], 'void', + 'cppverify::pre(%s(a, n) && 0 <= n && n <= 1000)\n' + 'cppverify::modifies(a[0 : n])\n' + 'cppverify::post(%s(k, 0, n, a[k] == %s))' % (V, FA, memset_value(t)), + 'memset(a, c, n * sizeof(%s));' % t, inputs=one_buffer(t, scalar='c'), + prelude='#include ', + post=(lambda t: lambda i, b, r: b[0] == [repeated(i['c'], t)] * i['n'])(t)) + case('l_memcmp_' + tag, + [('b', 'const ' + t, 'd', 'n'), ('b', 'const ' + t, 's', 'n'), ('s', 'int', 'n')], 'int', + 'cppverify::pre(%s(d, n) && %s(s, n) && 0 <= n && n <= 1000)\n' + 'cppverify::post((%s == 0) == %s(k, 0, n, d[k] == s[k]))' % (V, V, R, FA), + 'return memcmp(d, s, n * sizeof(%s));' % t, inputs=two_buffers(t, same=True), + prelude='#include ', + post=lambda i, b, r: (r == 0) == (i['d'] == i['s'])) + +case('l_memmove_left', [('b', 'int', 'a', 'n'), ('s', 'int', 'n')], 'void', + 'cppverify::pre(%s(a, n) && 1 <= n && n <= 1000)\n' + 'cppverify::modifies(a[0 : n])\n' + 'cppverify::post(%s(k, 0, n - 1, a[k] == %s(a[k + 1])))' % (V, FA, O), + 'memmove(a, a + 1, (n - 1) * sizeof(int));', + inputs=lambda: [d for d in one_buffer('int')() if d['n'] >= 1], + prelude='#include ', + post=lambda i, b, r: b[0][:-1] == i['a'][1:]) +case('l_memmove_right', [('b', 'short', 'a', 'n'), ('s', 'int', 'n')], 'void', + 'cppverify::pre(%s(a, n) && 1 <= n && n <= 1000)\n' + 'cppverify::modifies(a[0 : n])\n' + 'cppverify::post(%s(k, 1, n, a[k] == %s(a[k - 1])))' % (V, FA, O), + 'memmove(a + 1, a, (n - 1) * sizeof(short));', + inputs=lambda: [d for d in one_buffer('short')() if d['n'] >= 1], + prelude='#include ', + post=lambda i, b, r: b[0][1:] == i['a'][:-1]) +case('l_memcmp_order', [('b', 'const unsigned char', 'd', 'n'), + ('b', 'const unsigned char', 's', 'n'), ('s', 'int', 'n')], 'int', + 'cppverify::pre(%s(d, n) && %s(s, n) && 0 <= n && n <= 1000)\n' + 'cppverify::post(%s(j, 0, n, !%s(i, 0, j, d[i] == s[i]) || d[j] == s[j] || ' + '(%s < 0) == (d[j] < s[j])))' % (V, V, FA, FA, R), + 'return memcmp(d, s, n);', inputs=two_buffers('unsigned char', same=True), + prelude='#include ', + post=lambda i, b, r: (r < 0) == (i['d'] < i['s']) and (r == 0) == (i['d'] == i['s'])) +case('l_abs', [('s', 'int', 'x')], 'int', + 'cppverify::pre(x != -2147483647 - 1)\n' + 'cppverify::post(%s == (x < 0 ? -x : x))' % R, + 'return abs(x);', prelude='#include ', + inputs=[{'x': x} for x in [-2**31 + 1, -1000, -1, 0, 1, 1000, 2**31 - 1]], + pre=lambda i: i['x'] != -2**31, post=lambda i, b, r: r == abs(i['x'])) +case('l_labs', [('s', 'long', 'x')], 'long', + 'cppverify::pre(x != -9223372036854775807L - 1)\n' + 'cppverify::post(%s == (x < 0 ? -x : x))' % R, + 'return std::abs(x);', prelude='#include ', + inputs=[{'x': x} for x in [-2**63 + 1, -2**40, -1, 0, 1, 2**40, 2**63 - 1]], + pre=lambda i: i['x'] != -2**63, post=lambda i, b, r: r == abs(i['x'])) + +# False claims: none may verify, and a counterexample must be a real one. +case('l_memcpy_false', [('b', 'int', 'd', 'n'), ('b', 'const int', 's', 'n'), ('s', 'int', 'n')], 'void', + 'cppverify::pre(%s(d, n) && %s(s, n) && 1 <= n && n <= 1000)\n' + 'cppverify::modifies(d[0 : n])\n' + 'cppverify::post(d[0] == %s(d[0]))' % (V, V, O), + 'memcpy(d, s, n * sizeof(int));', inputs=two_buffers('int'), + prelude='#include ', + pre=lambda i: i['n'] >= 1, + post=lambda i, b, r: b[0][0] == i['d'][0]) +case('l_memset_false', [('b', 'int', 'a', 'n'), ('s', 'int', 'n'), ('s', 'int', 'c')], 'void', + 'cppverify::pre(%s(a, n) && 1 <= n && n <= 1000)\n' + 'cppverify::modifies(a[0 : n])\n' + 'cppverify::post(a[0] == c)' % V, + 'memset(a, c, n * sizeof(int));', inputs=one_buffer('int', scalar='c'), + prelude='#include ', + pre=lambda i: i['n'] >= 1, + post=lambda i, b, r: b[0][0] == i['c']) +case('l_memcmp_false', [('b', 'const int', 'd', 'n'), ('b', 'const int', 's', 'n'), ('s', 'int', 'n')], 'int', + 'cppverify::pre(%s(d, n) && %s(s, n) && 0 <= n && n <= 1000)\n' + 'cppverify::post(%s == 0)' % (V, V, R), + 'return memcmp(d, s, n * sizeof(int));', inputs=two_buffers('int', same=True), + prelude='#include ', + post=lambda i, b, r: r == 0) +case('l_abs_min', [('s', 'int', 'x')], 'int', + 'cppverify::post(%s >= 0)' % R, + 'return abs(x);', prelude='#include ', + inputs=[{'x': x} for x in [-2**31, -1, 0, 2**31 - 1]], + post=lambda i, b, r: r >= 0) + +CASES = C +CONFIGS = ('z3', 'bv', 'int', 'cvc5') diff --git a/clang/utils/cppverify-differential/run.py b/clang/utils/cppverify-differential/run.py index d6e20cb034..acf5c3646f 100644 --- a/clang/utils/cppverify-differential/run.py +++ b/clang/utils/cppverify-differential/run.py @@ -22,7 +22,8 @@ import differential # noqa: E402 SUITES = ['integers', 'shifts_division', 'contracts', 'loops', 'calls', 'pointers', - 'pointers_bmc', 'expressions', 'loops_bmc', 'bit_int', 'records', 'selftest'] + 'pointers_bmc', 'expressions', 'loops_bmc', 'bit_int', 'records', 'library', + 'selftest'] DEFAULT = [s for s in SUITES if s != 'selftest'] diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index a69f5e836e..8aadc978cf 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -375,6 +375,31 @@ types, and the parameters in `ValueReferences` are read as values; a function that cannot be lifted returns a placeholder that the lifting loop marks unsupported, so `SpecDependencies` name it. +**The C library's memory functions and abs:** a contract on `void *` cannot +speak of the objects behind it, and the heap keeps one cell per object, so +`convertLibraryCall` recognizes `memcpy`, `memmove`, `memset`, and `memcmp` +by builtin ID, reads the objects each pointer addresses as written, before +its conversion to `void *` (`beforeVoidPointer`; an enumeration as its +underlying integer), and lowers the call to a `VCallStmt` of that type's +model, a trusted declaration with a contract in `` +(`cppverify::model`, found by `libraryModel`), with `k = n / sizeof(T)` and +an `unsupported` assert, with its note (`VAssertStmt::Note`), that `n` is a +multiple of `sizeof(T)`. The pointers' objects must have one size, and be +`bool` on both sides or neither. `memset`'s byte becomes the object it +repeats, `(unsigned char)c * 0x0101...` reinterpreted as `T`. The main +conversion loop skips the models (`isLibraryModel`); the ones calls use +(`UsedLibraryModels`) are converted after it and marked `IsBuiltin`, so +they are neither verified nor reported, but stay trusted: established for +the fixpoint, and named in every caller's `[trusts=...]`. The modular call +then does the rest as for any callee: extents contained in the caller's +objects, the separation of `memcpy`'s ranges (`memmove`'s model has +`aliases`), the frame `d[0 : k]`, and the postconditions. `convertAbs` +lowers `abs`, `labs`, `llabs`, and `std::abs` of an integer (in `std`, or a +global `abs` of a system header, as libc++'s `` defines it) to +`x < 0 ? -x : x` in the parameter's type in the function's integer mode: +machine in executable and proof code, contracts included, where `-x` is +checked for overflow, and mathematical in a spec. + **Records in memory by value:** `recordFieldsInMemory` reads a record value kept in memory, a promoted local or one in a pointee or record reference (`promotedRootLocal`, `inPointeeObject`), through implicit copies and @@ -453,6 +478,20 @@ a synthesized spec (`IsBuiltin`, identity `__cppverify_table.@L:C` or `__cppverify_string@L:C`) whose body is a balanced comparison tree over the linear index. +**Bit builtins:** `ASTConverter::convertBitBuiltin` lowers a call of +`__builtin_clz`, `ctz`, `popcount`, `parity`, `ffs` (and their `l`/`ll` +forms) or `bswap16/32/64` to its definition over the operand, read as an +unsigned machine value of the parameter's width (a mathematical argument +converts to the parameter's type first, as a bitwise operand does): `clz` +and `ctz` are a ladder of conditionals on `x & 2^k != 0` with literal +results, `popcount` and `parity` a balanced sum of one-bit terms in a byte +(at most 64, so its adders stay small), and `bswap` the bits moved to their +places, combined with `|` since no two meet. None of these operations has a +check of its own. `clz` and `ctz` are wrapped in +`ite(Require(x != 0, builtin-argument), v, v)`, except in an explicit spec, +which is total and counts every bit of 0. Summing the bits at the operand's +width made `parity` of a `popcount` take 6 s; in a byte it takes 0.8 s. + **Require:** produced by the spec inliner from the `assert` statements of a lifted `constexpr` helper's body (`evalBodySeq`): on the path `g` to `assert(c)` it adds `Require(!g || c, kind)` to the evaluation @@ -2512,7 +2551,9 @@ around it (`PassiveStmt::Focus`, the condition's `Loc`, `BeginLoc`, and precondition at a call the call (`VCallStmt::CallSite`, the call expression, set by the converter's `atCall`) with the callee's clause (`PassiveStmt::Clause`); a call's own checks, whose conditions are anchored -at the call statement, take the call expression as their focus. Layer 3 +at the call statement, take the call expression as their focus. A check that +a postcondition is defined is anchored at the clause +(`PassiveExitAssert::Anchor`), and its operation is its focus. Layer 3 keeps both on the obligation (`Obligation::Focus`, `Clause`), as diagnostics only: archives keep their sources from schema v6, and hashes neither. When the driver annotates a module's sources it drops a focus that @@ -3011,9 +3052,22 @@ statement (a condition's before the `VIfStmt`), its arguments lowered as a call statement's are (`convertExecCallArgs`, nested calls into `__nested_N`), and the expression reads the temporary; a `CallExpr` converted twice within a statement, as an index the binding check reads again, calls once -(`HoistedCalls`). So `Passivize::emitCallStmt` applies callee +(`HoistedValues`). So `Passivize::emitCallStmt` applies callee `cppverify::pre`/`cppverify::post` at each site. +- **Writes.** An increment, a decrement, or an assignment whose value an + expression uses goes to the call sink the same way (`hoistSideEffect`): its + statement, converted as a statement of its own is, runs before the rest of + the expression, and its value is read into a temporary `__value_N` there, + a postfix operator's before the write and any other's after it. A comma's + first operand is converted as a discarded statement into the sink, and the + comma is its second operand. `HoistedValues` maps each hoisted call or + write to its temporary, so an expression the converter reads twice, as a + compound assignment's target is read and then located, is evaluated once. + The statement of a write continues its expression's evaluation and keeps + that map (`ContinuesEvaluation`), since its target is converted again in + it: `a[k++]++` increments `k` once. + - **Paths.** An operand that `&&`, `||`, or `?:` evaluates only on its own path is converted with both sinks pointed at a list of its own (`convertOnPaths`). When that list stays empty the operator is the @@ -3038,14 +3092,20 @@ statement, as an index the binding check reads again, calls once member function) beside an evaluation a call may change in the other (`isHeapSensitive`: a load, a reference, an addressable local, another call; for an assignment's target only what locating it reads, - `locatingIsHeapSensitive`) is a conversion error at the expression. An - assignment whose target makes a call saves its right operand in - `__value_N` before converting the target, so the value is read, and - checked, before the target's calls run, as C++17 sequences them. Frama-C + `locatingIsHeapSensitive`) is a conversion error at the expression. So is + a write in one operand that the other may read (`writesWhatReads`): a + variable it writes that the other names, with the fields of a record held + by value counted as the record's, or memory (a field through a pointer or + `this`, an element, a reference) beside an evaluation a call may change. + C++ leaves such a write and read + undefined. An assignment whose target makes a call or a write saves its + right operand in `__value_N` before converting the target, so the value + is read, and checked, before the target's calls and writes run, as C++17 + sequences them. Frama-C keeps such orders as CIL `UnspecifiedSequence` statements with the reads and writes of each part and checks them access by access under - `-unspecified-access`; the rule here is per call, coarser but needing no - read sets. + `-unspecified-access`; the rule here is per call and per written variable, + coarser but needing no read sets. - A call whose result is a record is lowered only as a statement, a whole initializer, assignment, or return value; one that returns nothing only as a statement. diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 140e81df35..ac1677ec82 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -278,6 +278,15 @@ old `*p`. A call returning a record is made only as a statement or a whole initializer, assignment, or return value, and one returning nothing only as a statement. +An increment, a decrement, an assignment, or a comma expression may stand +where its value is used in executable code (`a[i++]`, `*dst++ = *src++`, +`while (k-- > 0)`, `if ((c = *p) != 0)`, `a = b = 0`): its write runs where +C++ evaluates it, as a call does, and its value is read there, a postfix +operator's before the write. Each expression is evaluated once, so +`a[i++] += 1` increments `i` once. A write in one unsequenced operand that +another reads (`i++ + i`, which C++ leaves undefined) is an error, as is a +write to memory beside an operand that reads memory. + ## Loop Contracts: invariant / decreases @@ -504,6 +513,19 @@ value evaluates the value, and a value computed for nothing (`x + 1;`) is computed with its checks. `[[assume(e)]]` and `__builtin_assume(e)` make `e` false undefined, so `e` is asserted (kind `assertion`), then assumed. +### Bit builtins + +`__builtin_clz`, `__builtin_ctz`, `__builtin_popcount`, `__builtin_parity`, +`__builtin_ffs` (with their `l` and `ll` forms), and `__builtin_bswap16/32/64` +are their exact definitions over the operand's bits, as CBMC models them +rather than trusting a contract: comparisons with constants, conditionals, +and sums without carries, none of which needs a check of its own. GCC leaves +`__builtin_clz(0)` and `__builtin_ctz(0)` undefined, which is an obligation of +the definedness kind `builtin-argument` where the call is evaluated, as +Frama-C's libc specifies them with `requires x != 0`; in a spec, which is +total, they count every bit of 0, as C++20's `std::countl_zero` does. Other +builtins stay unsupported. + An uncontracted `constexpr` helper is lifted as a spec whose definedness is checked at each call by unfolding its body. Its `assert(c)` becomes, during that unfolding, a `Require(!path || c)` expression in the evaluation, true @@ -913,6 +935,19 @@ standard defines them ([alg.min.max]): `max(a, b)` is `a < b ? b : a` and Any other function of the standard library that is not a constant is an error naming it. +Of the C library, `abs`, `labs`, `llabs`, and `std::abs` of an integer are +their definition, undefined at the minimum, and in a spec the mathematical +absolute value; libc++ defines the `std::abs` of `long` and `long long` in +the global namespace of its ``, so a global `abs` declared in a +system header is it too, and one of the user's own is not. `memcpy`, `memmove`, `memset`, +and `memcmp` of objects of an integer type `T` (an enumeration as its +underlying type, `bool` only with `bool`), with a size of `k * sizeof(T)` +bytes, are calls of their models in ``: trusted declarations +with contracts, one per type, over `k` objects (Frama-C's libc states the +same over bytes, which this memory model, one value per object, does not +have). A proof that uses one names it in `[trusts=...]`. A size that splits +an object is `construct.unsupported`. + **Compile-time partial evaluation:** When a contract contains a `constexpr` call whose arguments are all constants, Clang evaluates it at compile time before the verifier sees it. A callee precondition instantiated at a call site is not such a call: there the argument is substituted for the parameter, and the solver settles the application from the lifted definition: diff --git a/website/source/book/part-ii/ch18-undefined-behavior.rst b/website/source/book/part-ii/ch18-undefined-behavior.rst index 59580e5fb7..02607763b1 100644 --- a/website/source/book/part-ii/ch18-undefined-behavior.rst +++ b/website/source/book/part-ii/ch18-undefined-behavior.rst @@ -231,6 +231,26 @@ Green }`` that is ``0`` or ``1``: cv::pre(k >= 0 && k <= 5) { return (Color)k; } // FAILS: k = 2 is not a Color +Builtins +-------- + +A builtin can be undefined for an argument too. GCC leaves the count of the +leading or trailing zero bits of 0 undefined, so ``__builtin_clz(x)`` and +``__builtin_ctz(x)`` must not see ``x == 0``, an obligation of kind +``builtin-argument`` at the call: + +.. cppverify-example: fails lowest + +.. code-block:: cpp + + int lowest(unsigned x) + cv::post(cv::result < 32) + { return __builtin_ctz(x); } // FAILS: x = 0 + +The other bit builtins, ``__builtin_popcount``, ``__builtin_parity``, +``__builtin_ffs``, and ``__builtin_bswap*``, are defined for every argument +(see :doc:`../../language/functions-loops`). + Signed vs. unsigned ------------------- diff --git a/website/source/language/functions-loops.rst b/website/source/language/functions-loops.rst index 0c23b91164..89e5b80a34 100644 --- a/website/source/language/functions-loops.rst +++ b/website/source/language/functions-loops.rst @@ -42,6 +42,54 @@ type trait such as ``__is_same(T, U)``, ``offsetof``, and aliases, using-declarations, and local classes and enumerations declare names and do nothing at run time. +GCC's bit builtins are their exact definitions over the operand's bits: +``__builtin_clz``, ``__builtin_ctz``, ``__builtin_popcount``, +``__builtin_parity``, and ``__builtin_ffs``, each with its ``l`` and ``ll`` +forms, and ``__builtin_bswap16``, ``__builtin_bswap32``, and +``__builtin_bswap64``. GCC leaves the count of the leading or trailing zeros +of 0 undefined, so ``__builtin_clz`` and ``__builtin_ctz`` check, where they +are called, that their argument is not 0, a check of kind +``builtin-argument``. In a spec, which is total, they count every bit of 0 +as zero, as C++20's ``std::countl_zero`` and ``std::countr_zero`` do. + +.. code-block:: cpp + + namespace cv = cppverify; + + int log2_floor(unsigned x) + cv::pre(x != 0) + cv::post(0 <= cv::result && cv::result < 32) + cv::post(x >= 1u << cv::result) + { + return 31 - __builtin_clz(x); + } + + int top_bit(unsigned x) + cv::post(cv::result >= 0) + { + return 31 - __builtin_clz(x); + } + + bool one_bit(unsigned x) + cv::post(cv::result == (x != 0 && (x & (x - 1)) == 0)) + { + return __builtin_popcount(x) == 1; + } + +.. code-block:: text + + Verified: log2_floor [backend=z3] + bits.cpp:14:15: error: verification failed: top_bit [builtin-argument] [backend=z3] [reason=counterexample] + 14 | return 31 - __builtin_clz(x); + | ^~~~~~~~~~~~~~~~ + bits.cpp:14:15: note: counterexample: x = 0 + Verified: one_bit [backend=z3] + Summary: 2 verified, 1 failed in 0.2 s + +Before 0.2 a call of one of them stopped its function (``call to function +without a verification contract: __builtin_clz``), and a ``static_assert`` +with a message stopped the run. + A caller's proof uses its callees' contracts, so a verdict is only as good as those contracts. A caller whose proof relies on a callee contract that the callee's own verification did not establish is ``Unresolved`` with reason @@ -531,7 +579,7 @@ an operand that reads memory, or makes another call, is an error: .. code-block:: text - order.cpp:18:10: error: sum_with: C++ leaves the order of these operands open, and a call in one may write what the other reads; make the call in a statement of its own first + order.cpp:18:10: error: sum_with: C++ leaves the order of these operands open, and a call or a write in one may change what the other reads; make it a statement of its own first 18 | return add_one(p) + *p; | ^~~~~~~~~~~~~~~ @@ -562,8 +610,8 @@ the target is located: Before C++17 an assignment's operands are unsequenced too: with ``--extra-arg=-std=c++14``, ``store_old`` is ``error: store_old: before -C++17 the order of an assignment's operands is open, and a call in one may -write what the other reads; make the call in a statement of its own +C++17 the order of an assignment's operands is open, and a call or a write +in one may change what the other reads; make it a statement of its own first``. A call that returns nothing is made as a statement of its own @@ -574,6 +622,86 @@ initializer, assignment, or return value (``Pt p = make(x);``, context``. Before 0.2, every call inside a larger expression was that error, and the file stopped. +Writes in expressions +--------------------- + +An increment, a decrement, an assignment, or a comma expression may stand +where its value is used, as C code often writes it: ``a[i++]``, +``*dst++ = *src++``, ``while (k-- > 0)``, ``if ((c = *p) != 0)``, +``a = b = 0``. Its write runs where C++ evaluates it, as a call does: before +what reads its value, and under ``&&``, ``||``, or ``?:`` only on its own +path. Its value is read there: a postfix operator's is the value before the +write, any other's the value after it. + +.. code-block:: cpp + + void copy(int *dst, const int *src, int n) + cv::pre(cv::valid(dst, n) && cv::valid(src, n) && 0 <= n && n < 1000) + cv::modifies(dst[0 : n]) + cv::post(cv::forall(k, 0, n, dst[k] == src[k])) + { + int *d = dst; + const int *s = src; + for (int i = 0; i < n; i = i + 1) + cv::invariant(0 <= i && i <= n && d == dst + i && s == src + i) + cv::invariant(cv::forall(k, 0, i, dst[k] == src[k])) + cv::decreases(n - i) + { + *d++ = *s++; + } + } + + int countdown(int k) + cv::pre(0 <= k && k < 100) + cv::post(cv::result == 0) + { + while (k-- > 0) + cv::invariant(0 <= k && k < 100) + cv::decreases(k) + { + } + return k + 1; + } + +.. code-block:: text + + Verified: copy [backend=z3] + Verified: countdown [backend=z3] + +The condition ``k-- > 0`` decrements ``k`` at every test, the last one +included, so ``k`` is ``-1`` after the loop. + +Each expression is evaluated once, however often the verifier reads it: in +``a[i++] += 1`` the target is read and written, and ``i`` grows by one. An +assignment evaluates its right operand before its target (C++17), so +``a[k++] = k`` stores the old ``k`` at the old ``k``; before C++17 the two are +unsequenced, and a write in one that the other reads is the error above. + +The operands of most operators and the arguments of a call are unsequenced, +and C++ leaves a write to an object that another of them reads undefined. As +with a call that may write what another operand reads, that is an error at +the expression: + +.. cppverify-example: rejects + +.. code-block:: cpp + + int twice(int i) + cv::pre(0 <= i && i < 100) + { + return i++ + i; + } + +.. code-block:: text + + twice.cpp:4:10: error: twice: C++ leaves the order of these operands open, and a call or a write in one may change what the other reads; make it a statement of its own first + +Writes are values in executable code only: ghost code and proof functions +assign their locals in statements of their own, and a pointer to dynamic +storage (``new``) is assigned in a statement of its own. Before 0.2, each of +these forms was ``unsupported unary operator`` or ``unsupported binary +operator``, and its function was not verified. + Templates --------- diff --git a/website/source/language/limitations.rst b/website/source/language/limitations.rst index 0e85aecf39..00d05c7457 100644 --- a/website/source/language/limitations.rst +++ b/website/source/language/limitations.rst @@ -122,12 +122,19 @@ C++ feature boundaries requires-expression, a concept, a type trait, ``offsetof``, ``__builtin_LINE()``), template value parameters, default arguments and default member initializers, - ``__builtin_expect``, a record returned from an initializer list - (``return Pt{a, b};``), structured bindings that copy a record, and + ``__builtin_expect``, the bit builtins (``__builtin_clz``, + ``__builtin_ctz``, ``__builtin_popcount``, ``__builtin_parity``, + ``__builtin_ffs``, their ``l`` and ``ll`` forms, and + ``__builtin_bswap16/32/64``), a record returned from an initializer list + (``return Pt{a, b};``), structured bindings that copy a record, declarations that do nothing (``static_assert``, type aliases, - using-declarations, local classes and enumerations). - - The value of an assignment, an increment, or a comma expression - inside an expression (``a = b = 0``, ``*p++``); a pointer into a + using-declarations, local classes and enumerations), and the value of + an assignment, an increment or decrement, or a comma expression in + executable code (``a = b = 0``, ``*dst++ = *src++``, + ``while (k-- > 0)``), in C++'s order of evaluation. + - Such a value in ghost and proof code, or of an assignment of a pointer + to dynamic storage; a write that another unsequenced operand may read + (an error, as C++ leaves it undefined); a pointer into a string literal (its characters are read by index); other builtins; structured bindings of an array, of a tuple-like type, or by reference. @@ -573,8 +580,9 @@ it is evaluated (see :doc:`functions-loops`). Together they are not yet comprehensive C++ undefined-behavior checking. Missing general UB semantics include object provenance outside the represented -fragment, strict aliasing, arbitrary alignment, unsequenced side effects and -all unspecified evaluation-order alternatives, object lifetime restart, +fragment, strict aliasing, arbitrary alignment, unsequenced side effects +(rejected where one may meet another write or read, not checked) and all +unspecified evaluation-order alternatives, object lifetime restart, exception unwinding, floating-point environment, volatile/atomics, and data races. @@ -679,7 +687,10 @@ Libraries and real programs CppVerify does not yet ship comprehensive libc or C++ standard-library models: of the standard library it knows ``std::min`` and ``std::max`` of two integers (:doc:`functions-loops`), and any other of its functions is an -error naming it. An uncontracted call fails closed; a contract is assumed +error naming it. Of the C library it knows ``abs`` and the memory functions +``memcpy``, ``memmove``, ``memset``, and ``memcmp`` over integers, through +trusted models in ```` that every proof using one names +(:doc:`pointers`). An uncontracted call fails closed; a contract is assumed only when it is marked ``[[cppverify::trusted]]``, or, in one run over several files, once the verification of its definition in another of them establishes it, and for files verified apart once @@ -691,7 +702,8 @@ verification contract``). Broader application verification needs: -- memory/string primitives such as ``memcpy``, ``memmove``, and ``memset``; +- the memory functions over records and pointers, and the string functions + (``strlen``, ``strcmp``); - views of standard containers as the spec collections of ````; - ``std::array``, ``std::span``, smart pointers, optionals, and string views; - vectors, strings, associative containers, iterators, invalidation, and diff --git a/website/source/language/pointers.rst b/website/source/language/pointers.rst index 7ccc0bf854..cd09235903 100644 --- a/website/source/language/pointers.rst +++ b/website/source/language/pointers.rst @@ -636,6 +636,70 @@ pointer is null or an extent is empty, and every caller must prove that. An Addresses are reasoned about as mathematical integers, so range conditions like the non-overlap above are exact (no wraparound). +The C library's memory functions +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +``memcpy``, ``memmove``, ``memset``, and ``memcmp`` (and ``std::memcpy`` +and the others, and their ``__builtin_`` forms) work on whole objects of an +integer, enumeration, or ``bool`` type: a call whose pointers, as written +before their conversion to ``void *``, address objects of one size, with a +size of ``k * sizeof(T)`` bytes, is a call of the function's model for ``T`` +with ``k``. The models are declarations in ```` (namespace +``cppverify::model``), with contracts: + +- ``memcpy(d, s, k)``: ``d`` and ``s`` each point to ``k`` objects, which do + not overlap (as every two pointer parameters of which one is mutable); it + writes ``d[0 : k]``, and each ``d[i]`` is the ``s[i]`` of before the call; +- ``memmove``: the same, and the two may overlap; +- ``memset(d, c, n)``: each object is the byte ``(unsigned char)c`` repeated, + ``-1`` for ``memset(a, 0xff, ...)`` of ``int``; of ``bool``, whose only + values are 0 and 1, it is not modeled; +- ``memcmp``: 0 exactly when the objects are equal; of bytes, negative + exactly when the first difference is smaller, as ``unsigned char``. Of + wider objects that depends on the byte order, and is not modeled. + +The models are trusted, as the C library is: a proof that uses one names it. + +.. code-block:: cpp + + #include + + void copy(int *dst, const int *src, int n) + cv::pre(cv::valid(dst, n) && cv::valid(src, n) && 0 <= n && n <= 1000) + cv::modifies(dst[0 : n]) + cv::post(cv::forall(k, 0, n, dst[k] == src[k])) + { + memcpy(dst, src, n * sizeof(int)); + } + + bool same(const int *a, const int *b, int n) + cv::pre(cv::valid(a, n) && cv::valid(b, n) && 0 <= n && n <= 1000) + cv::post(cv::result == cv::forall(k, 0, n, a[k] == b[k])) + { + return memcmp(a, b, n * sizeof(int)) == 0; + } + +.. code-block:: text + + Verified: copy [backend=z3] [trusts=memcpy] + Verified: same [backend=z3] [trusts=memcmp] + +A copy whose ranges overlap fails the call's ``aliasing`` check, one past the +end of an extent its ``precondition``, and a size that splits an object +(``memcpy(d, s, 6)`` of ``int``) is defined C++ that the verifier, which keeps +one value per object, does not represent: ``construct.unsupported``. Records +and pointers are not modeled yet (``memcpy of 'Pt *' and 'const Pt *' is +unsupported``), nor are the string functions (``strlen``, ``strcmp``). + +``abs``, ``labs``, ``llabs``, and ``std::abs`` of an integer are their +definition, ``x < 0 ? -x : x`` in the parameter's type, whether the library +defines ``std::abs`` in ``std`` (libstdc++) or in the global namespace of its +```` (libc++, so on macOS); an ``abs`` of your own is a function like +any other: ``abs(INT_MIN)`` is +an ``overflow``, in a contract too. In a spec, whose integers are +mathematical, it is the absolute value, so a spec's ``abs(-2147483648)`` is +``2147483648``. + Same-array pointer difference ----------------------------- diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst index dbc1b93fc2..52e22c30a6 100644 --- a/website/source/language/tooling.rst +++ b/website/source/language/tooling.rst @@ -1212,7 +1212,8 @@ kind says what the check is: - C++ definedness: ``overflow`` (including a mathematical value converted to a machine type it does not fit), ``division-by-zero``, ``shift``, ``bounds``, ``dereference``, ``initialization``, ``pointer-difference``, - and ``deallocation``; + ``deallocation``, and ``builtin-argument`` (an argument a builtin is + undefined for, such as ``__builtin_clz(0)``); - generated interfaces: ``pointer-validity`` (a pointer parameter, result, or ``valid(p, n)`` extent must denote valid storage), ``aliasing`` (implicit non-aliasing), ``frame`` (writes and callee effects stay within diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index b271d4edb8..650570c175 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -561,6 +561,38 @@ does not hold (``x % 2 == 0``); JSON gives that clause as ``related``, SARIF as a related location. A call's step on the path is at the call too. The check's ID keeps its anchor (:doc:`language/tooling`). +**Bit builtins.** A call of ``__builtin_clz``, ``__builtin_ctz``, +``__builtin_popcount``, ``__builtin_parity``, ``__builtin_ffs`` (each with +its ``l`` and ``ll`` forms), or ``__builtin_bswap16/32/64`` stopped its +function (``call to function without a verification contract``). Each is now +its exact definition over the operand's bits, and ``__builtin_clz`` and +``__builtin_ctz`` of 0, which GCC leaves undefined, fail a check of the new +kind ``builtin-argument`` at the call. A ``static_assert`` with a message in a +function crashed cpp-verify; it now does nothing, as one without a message +did (:doc:`language/functions-loops`). + +**Writes in expressions.** The value of an increment, a decrement, an +assignment, or a comma expression inside a larger expression (``a[i++]``, +``*dst++ = *src++``, ``while (k-- > 0)``, ``if ((c = *p) != 0)``, +``a = b = 0``) stopped its function (``unsupported unary operator``, +``unsupported binary operator``). Each write now runs where C++ evaluates it, +a ``&&``, ``||``, or ``?:`` operand's only on its path, and its value is read +there, a postfix operator's before the write. An expression the verifier +reads twice, as a compound assignment's target, is still evaluated once. +Where C++ leaves the order of operands open, a write that another operand may +read is an error at the expression, as such a call already was +(:doc:`language/functions-loops`). + +**The C library's memory functions.** A call of ``memcpy``, ``memmove``, +``memset``, ``memcmp``, or ``abs`` stopped its function (``call to function +without a verification contract``). Over arrays of integers, enumerations, +or ``bool``, the memory functions are now calls of their models, contracted +declarations in ```` for each type of object, trusted like the +library itself, so a proof that uses one shows it (``[trusts=memcpy]``); a +copy whose ranges overlap fails its ``aliasing`` check. ``abs`` is its +definition, with an ``overflow`` check at the minimum. Records, pointers, and +the string functions are not modeled yet (:doc:`language/pointers`). + **cvc5's counterexamples.** A failure cvc5 found (``--backend=cvc5``, or a race cvc5 won) gave no values and no path: the certifier checked its model and the verifier then dropped it, so the JSON record had no ``model`` or ``trace``,