diff --git a/clang/lib/Verify/Frontend/ASTConverter.cpp b/clang/lib/Verify/Frontend/ASTConverter.cpp index f03a5b820d..2b2c997140 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.cpp +++ b/clang/lib/Verify/Frontend/ASTConverter.cpp @@ -519,9 +519,11 @@ isSupportedVerificationTypeImpl(QualType Ty, const RecordDecl *RD = RT->getDecl()->getDefinition(); if (!RD || RD->isUnion()) return false; + // Copies of the object are its bytes and its lifetime ends without a + // destructor; its constructors run as calls or as their initializers. if (const auto *CXXRD = dyn_cast(RD)) if (CXXRD->getNumBases() != 0 || CXXRD->isPolymorphic() || - !CXXRD->isTrivial() || !CXXRD->isStandardLayout()) + !CXXRD->isTriviallyCopyable() || !CXXRD->isStandardLayout()) return false; if (!Visiting.insert(Ty.getTypePtr()).second) return true; @@ -595,6 +597,27 @@ static bool isPromotableAggregateType(QualType Ty, const ASTContext &Ctx) { isFlattenedRecordType(Canonical); } +/// The constructor call an initializer is, through the wrappers that do +/// not change the object: parentheses, cleanups, and a conversion by a +/// constructor (`T x = T(5);`). +static const CXXConstructExpr *constructionOf(const Expr *Init) { + while (Init) { + Init = Init->IgnoreParens(); + if (const auto *Cleanups = dyn_cast(Init)) { + Init = Cleanups->getSubExpr(); + continue; + } + if (const auto *Cast = dyn_cast(Init); + Cast && (Cast->getCastKind() == CK_ConstructorConversion || + Cast->getCastKind() == CK_NoOp)) { + Init = Cast->getSubExpr(); + continue; + } + return dyn_cast(Init); + } + return nullptr; +} + /// Largest automatic object the byte-granular allocation metadata can describe. static constexpr uint64_t MaxAutomaticObjectBytes = 256; @@ -1441,6 +1464,12 @@ void ASTConverter::beginInitializationTracking(const FunctionDecl *FD) { // flattened SSA representation at all. if (VD->hasLocalStorage() && VD->getType()->isArrayType()) addObject(VD); + // A constructor that is not trivial runs on the object's address. + if (const auto *Construct = + VD->hasInit() ? constructionOf(VD->getInit()) : nullptr; + Construct && Construct->getConstructor() && + !Construct->getConstructor()->isTrivial()) + addObject(VD); return true; } @@ -1961,12 +1990,65 @@ static void markUnsupported(VFunction &Fn) { /// static member is a free function, and a non-static one of a class without /// bases or virtual functions is a function of `this`, a pointer to its /// object. +/// Why a constructor is not verified, or nothing: its class has no bases +/// or virtual functions, it does not delegate, and each member is a scalar, +/// a pointer, or an aggregate of them, initialized by expressions or by +/// constructors the class does not provide itself. +static std::optional +unsupportedConstructor(const CXXConstructorDecl *Ctor) { + const CXXRecordDecl *Class = Ctor->getParent(); + if (!Class->hasDefinition() || Class->getNumBases() != 0 || + Class->isPolymorphic()) + return std::string("member functions of a class with bases or virtual " + "functions are unsupported"); + if (!Class->isTriviallyCopyable()) + return std::string("constructors of a class that is not trivially " + "copyable, whose copies or destruction run code, are " + "not supported yet"); + if (Ctor->isDelegatingConstructor()) + return std::string("delegating constructors are not verified yet"); + for (const FieldDecl *Field : Class->fields()) { + if (Field->getType()->isReferenceType()) + return std::string("constructors of a class with reference members are " + "unsupported"); + if (Field->isBitField()) + return std::string("constructors of a class with bit-field members are " + "unsupported"); + if (const CXXRecordDecl *Member = + Field->getType()->getBaseElementTypeUnsafe()->getAsCXXRecordDecl()) + if (llvm::any_of(Member->ctors(), [](const CXXConstructorDecl *C) { + return C->isUserProvided(); + })) + return std::string("members whose class provides a constructor are " + "not supported yet"); + } + for (const CXXCtorInitializer *Init : Ctor->inits()) + if (!Init->isMemberInitializer()) + return std::string("constructors of a class with anonymous members are " + "unsupported"); + return std::nullopt; +} + +static bool mentionsThis(const Stmt *S) { + if (!S) + return false; + if (isa(S)) + return true; + return llvm::any_of(S->children(), + [](const Stmt *Child) { return mentionsThis(Child); }); +} + +/// The lifetime companion of a constructor's object, whose lifetime begins +/// at `this` when the constructor is entered. +static constexpr const char *ConstructedObjectLifetime = + "__cppverify_constructed_lifetime"; + static std::optional unsupportedMemberFunction(const CXXMethodDecl *Method) { if (Method->getParent()->isLambda()) return std::string("lambdas are unsupported"); - if (isa(Method)) - return std::string("constructors are not verified yet"); + if (const auto *Ctor = dyn_cast(Method)) + return unsupportedConstructor(Ctor); if (isa(Method)) return std::string("destructors are not verified yet"); if (isa(Method)) @@ -2439,8 +2521,8 @@ bool ASTConverter::flattenRecordInto(const RecordDecl *RD, if (!Definition || Definition->isUnion()) return false; if (const auto *CXX = dyn_cast(Definition)) - if (CXX->getNumBases() != 0 || CXX->isPolymorphic() || !CXX->isTrivial() || - !CXX->isStandardLayout()) + if (CXX->getNumBases() != 0 || CXX->isPolymorphic() || + !CXX->isTriviallyCopyable() || !CXX->isStandardLayout()) return false; const ASTRecordLayout &RL = Ctx.getASTRecordLayout(Definition); unsigned Index = 0; @@ -2674,7 +2756,8 @@ bool ASTConverter::exceedsNestingLimit(const FunctionDecl *FD, } /// The address parameter and the fields of a pointer field of the object it -/// addresses (s->data, s.data for a reference s, s->inner.data, (*s).data), +/// addresses (s->data, s.data for a reference s, s->inner.data, (*s).data, +/// and this->data in a member function, with no parameter declaration), /// whose pointee is a complete object type. static std::optional< std::pair>> @@ -2696,6 +2779,8 @@ pointerFieldOfParameter(const Expr *E) { return std::nullopt; Fields.insert(Fields.begin(), Field); if (M->isArrow()) { + if (isa(M->getBase()->IgnoreParenImpCasts())) + return std::make_pair(nullptr, std::move(Fields)); // p->f: the object p, a pointer parameter, addresses. const ParmVarDecl *P = Parameter(M->getBase()); if (!P || !P->getType()->isPointerType()) @@ -2721,6 +2806,7 @@ pointerFieldOfParameter(const Expr *E) { std::vector ASTConverter::collectFieldExtents(const FunctionContractInfo &FCI, + llvm::ArrayRef Invariants, VFunction &Fn) { struct MarkerFinder : RecursiveASTVisitor { std::vector Pointers; @@ -2734,17 +2820,20 @@ ASTConverter::collectFieldExtents(const FunctionContractInfo &FCI, } Finder; for (const Expr *Pre : FCI.Preconditions) Finder.TraverseStmt(const_cast(Pre)); + for (const Expr *Invariant : Invariants) + Finder.TraverseStmt(const_cast(Invariant)); std::vector Out; for (const Expr *Pointer : Finder.Pointers) { auto Field = pointerFieldOfParameter(Pointer); if (!Field) continue; const auto &[Param, Fields] = *Field; - std::string Name = valueName(Param); - std::string Display = Param->getNameAsString(); + std::string Name = Param ? valueName(Param) : "this"; + std::string Display = Param ? Param->getNameAsString() : "this"; + const bool ThroughPointer = !Param || Param->getType()->isPointerType(); for (size_t I = 0; I != Fields.size(); ++I) { Name += "->" + Fields[I]->getNameAsString(); - Display += (I == 0 && Param->getType()->isPointerType() ? "->" : ".") + + Display += (I == 0 && ThroughPointer ? "->" : ".") + Fields[I]->getNameAsString(); } const Expr *Key = Pointer->IgnoreParenImpCasts(); @@ -2773,6 +2862,34 @@ ASTConverter::collectFieldExtents(const FunctionContractInfo &FCI, return Out; } +/// The class invariants a member function assumes on entry: a public one's, +/// unless it is a constructor. +std::vector +ASTConverter::entryClassInvariants(const CXXMethodDecl *Method, + bool Constructor) const { + if (!Method || !Method->isInstance() || Constructor || + Method->getAccess() != AS_public) + return {}; + const TypeContractInfo *TCI = Ctx.getTypeContract(Method->getParent()); + return TCI ? std::vector(TCI->Invariants.begin(), + TCI->Invariants.end()) + : std::vector(); +} + +/// The class invariants a member function must hold at exit: a public +/// one's, and every constructor's. +std::vector +ASTConverter::exitClassInvariants(const CXXMethodDecl *Method, + bool Constructor) const { + if (!Method || !Method->isInstance() || + (!Constructor && Method->getAccess() != AS_public)) + return {}; + const TypeContractInfo *TCI = Ctx.getTypeContract(Method->getParent()); + return TCI ? std::vector(TCI->Invariants.begin(), + TCI->Invariants.end()) + : std::vector(); +} + std::unique_ptr ASTConverter::convertFunction(const FunctionDecl *FD) { llvm::SaveAndRestore At(CurrentRange, SourceRange(FD->getLocation())); @@ -2842,6 +2959,8 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { // function of `this`, the pointer to its object. const auto *Method = dyn_cast(FD); const bool HasThis = Method && Method->isInstance(); + const auto *Constructor = dyn_cast(FD); + Fn->IsConstructor = Constructor != nullptr; Fn->Name = Method ? FD->getQualifiedNameAsString() : FD->getNameAsString(); Fn->Identity = functionIdentity(FD); Fn->IsSpec = FCI->IsSpec; @@ -2936,7 +3055,8 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { Addresses.push_back( {valueName(P), addressedType(P), isMutableAddressParam(P)}); if (FCI && !Fn->IsSpec) - for (AddressEntry &Field : collectFieldExtents(*FCI, *Fn)) + for (AddressEntry &Field : collectFieldExtents( + *FCI, entryClassInvariants(Method, Constructor), *Fn)) Addresses.push_back(std::move(Field)); if (Fn->ReturnType.Kind == VTypeKind::Struct) { for (const auto &[Field, Type] : Fn->ReturnFields) @@ -2960,6 +3080,13 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { }; InPost = false; + // A constructor's precondition is evaluated before its object exists. + if (Constructor) + for (const Expr *E : FCI->Preconditions) + if (mentionsThis(E)) + error(E->getExprLoc(), + Fn->Name + ": a constructor's precondition cannot read its " + "object, whose lifetime has not begun"); for (const Expr *E : FCI->Preconditions) { std::unique_ptr PE; recordContractExpr("pre", E, PE); @@ -2997,8 +3124,10 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { // write its object; a const one only its own storage. An explicit modifies // replaces the default, and a trusted or bodiless one keeps the rule of a // trusted contract. - if (HasThis && !ThisObject.isConstQualified() && FCI->Modifies.empty() && - FD->hasBody() && !Fn->IsTrusted) { + // A constructor always writes its object. + if (HasThis && !ThisObject.isConstQualified() && + ((FCI->Modifies.empty() && FD->hasBody() && !Fn->IsTrusted) || + Constructor)) { VFootprint Object; Object.Target = std::make_unique( std::make_unique("this", Fn->Params.front().second, @@ -3049,6 +3178,10 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { } Fn->InductiveLoc = FCI->Inductive; for (const auto &Pair : FCI->Aliases) { + if (Constructor && (mentionsThis(Pair.first) || mentionsThis(Pair.second))) + error(Pair.first->getExprLoc(), + Fn->Name + ": a constructor's object is new, so aliases cannot " + "name this"); std::unique_ptr L; std::unique_ptr R; recordContractExpr("aliases", Pair.first, L); @@ -3068,18 +3201,58 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { VBinOp::Ne, This(), std::make_unique(0, VType::makePtr(), SourceLocation()), VType::makeBool(), SourceLocation()); - auto Readable = std::make_unique( + std::unique_ptr Readable = std::make_unique( VBinOp::And, std::make_unique(VUnaryOp::ValidPtr, This(), VType::makeBool(), SourceLocation()), std::make_unique(VUnaryOp::InitializedPtr, This(), VType::makeBool(), SourceLocation()), VType::makeBool(), SourceLocation()); + // A constructor's object is storage the caller allocated, one live + // allocation at every leaf, which the constructor initializes: `this` + // carries that allocation's identity. + if (Constructor) { + VVarExpr Object("this", VType::makePtr(), SourceLocation(), + ConstructedObjectLifetime); + Readable = nullptr; + forEachObjectLeaf(ThisObject, 0, [&](QualType, uint64_t Offset) { + auto Leaf = std::make_unique( + VUnaryOp::ValidPtr, + objectLeafAddress(&Object, Offset, SourceLocation()), + VType::makeBool(), SourceLocation()); + if (Readable) + Readable = std::make_unique( + VBinOp::And, std::move(Readable), std::move(Leaf), + VType::makeBool(), SourceLocation()); + else + Readable = std::move(Leaf); + return true; + }); + if (!Readable) + Readable = std::make_unique(1, VType::makeBool(), + SourceLocation()); + } addPrecondition(*Fn, std::make_unique( VBinOp::And, std::move(NonNull), std::move(Readable), VType::makeBool(), SourceLocation()), ProofObligationKind::PointerValidity); + // A class invariant holds at the boundary of every public member + // function and is established by every constructor. It is checked at + // every call, internal ones included, so no call can observe the + // object while a member function breaks it. + FieldSubstPrefix.clear(); + for (const Expr *Invariant : entryClassInvariants(Method, Constructor)) + if (auto Pre = convertTypeInvariantExpr(Invariant)) + addPrecondition(*Fn, std::move(Pre), + ProofObligationKind::TypeInvariant); + // At exit an extent marker states nothing, and the next call checks + // the extent from what its caller knows. + llvm::SaveAndRestore DropMarkers(DropExtentMarkers, true); + for (const Expr *Invariant : exitClassInvariants(Method, Constructor)) + if (auto Post = convertTypeInvariantExpr(Invariant)) + addPostcondition(*Fn, std::move(Post), + ProofObligationKind::TypeInvariant); } for (const ParmVarDecl *P : AddressParams) { auto Pointer = std::make_unique(valueName(P), VType::makePtr(), @@ -3240,6 +3413,20 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { std::move(Condition), Check->getExprLoc())); } ErrorInContract = false; + // A constructor's member initializers run before its body, on an object + // of which nothing is known to be initialized. + if (Constructor) { + if (Ctx.getTypeSizeInChars(ThisObject).getQuantity() > + static_cast(MaxAutomaticObjectBytes)) + error(FD->getLocation(), Fn->Name + + ": constructors of a class larger than " + + std::to_string(MaxAutomaticObjectBytes) + + " bytes are not supported yet"); + VVarExpr This("this", Fn->Params.front().second, FD->getLocation(), + ConstructedObjectLifetime); + appendMemberInitializers(Constructor, &This, 0, FD->getLocation(), + Fn->Body); + } for (auto &S : convertStmt(Body)) Fn->Body.push_back(std::move(S)); TrackInitialization = false; @@ -4364,6 +4551,15 @@ std::unique_ptr ASTConverter::convertExpr(const Expr *E) { llvm::SaveAndRestore At(CurrentRange, E && E->getSourceRange().isValid() ? E->getSourceRange() : CurrentRange); + if (DropExtentMarkers) + if (const auto *Call = dyn_cast_or_null( + E ? E->IgnoreParenImpCasts() : nullptr)) { + const FunctionDecl *Callee = Call->getDirectCallee(); + if (Callee && Callee->getDeclName().isIdentifier() && + Callee->getName() == "valid" && Call->getNumArgs() == 2) + return std::make_unique(1, VType::makeBool(), + E->getExprLoc()); + } // An extent marker's pointer field is its entry value's parameter. if (E && !FieldExtentParameters.empty()) if (auto It = FieldExtentParameters.find(E->IgnoreParenImpCasts()); @@ -5035,8 +5231,9 @@ std::unique_ptr ASTConverter::convertExprImpl(const Expr *E) { : std::string("unsupported use of this")); return nullptr; } - return std::make_unique("this", CurrentFn->Params.front().second, - E->getExprLoc()); + return std::make_unique( + "this", CurrentFn->Params.front().second, E->getExprLoc(), + CurrentFn->IsConstructor ? ConstructedObjectLifetime : ""); } if (const auto *Decay = dyn_cast(E); Decay && Decay->getCastKind() == CK_ArrayToPointerDecay) { @@ -5970,9 +6167,70 @@ void ASTConverter::convertExecCallArgs( } } +std::optional ASTConverter::recordFieldsInMemory( + const Expr *E, SourceLocation Loc, + std::vector>> &Fields) { + // A copy of the record, implicit or defaulted, is its fields. + while (E) { + E = E->IgnoreParens(); + if (const auto *Cast = dyn_cast(E); + Cast && (Cast->getCastKind() == CK_NoOp || + Cast->getCastKind() == CK_LValueToRValue)) { + E = Cast->getSubExpr(); + continue; + } + if (const auto *Temporary = dyn_cast(E)) { + E = Temporary->getSubExpr(); + continue; + } + if (const auto *Construct = dyn_cast(E); + Construct && Construct->getNumArgs() == 1 && + Construct->getConstructor() && + !Construct->getConstructor()->isUserProvided() && + (Construct->getConstructor()->isCopyConstructor() || + Construct->getConstructor()->isMoveConstructor())) { + E = Construct->getArg(0); + continue; + } + break; + } + if (!E || (!promotedRootLocal(E) && !inPointeeObject(E))) + return std::nullopt; + const RecordDecl *Record = getRecordFromType(E->getType()); + const RecordDecl *Definition = Record ? Record->getDefinition() : nullptr; + if (!Definition) + return std::nullopt; + auto Place = objectPlace(E); + if (!Place) + return false; + std::unique_ptr AccessCondition = Place->takeAccessCondition(); + std::unique_ptr Base = Place->takeAddress(); + for (const FieldDecl *Field : Definition->fields()) { + auto Offset = recordFieldOffset(Field); + VType FieldType = VType::fromQualType(Field->getType(), IntMode, Ctx); + if (!Offset || FieldType.isAggregate() || + FieldType.Kind == VTypeKind::Unsupported) { + error(CurrentFn->Name + ": a record value read from memory must have " + "scalar fields"); + return false; + } + Fields.emplace_back(Field, std::make_unique( + objectLeafAddress(Base.get(), *Offset, Loc), + FieldType, Loc, "", + cloneVExpr(AccessCondition.get()))); + } + return true; +} + bool ASTConverter::appendRecordCallArgument( const Expr *E, const ParmVarDecl *Formal, std::vector> &Args) { + std::vector>> Fields; + if (auto InMemory = recordFieldsInMemory(E, E->getExprLoc(), Fields)) { + for (auto &Field : Fields) + Args.push_back(std::move(Field.second)); + return *InMemory; + } auto Base = convertExpr(E); if (!Base) return false; @@ -6307,37 +6565,21 @@ bool ASTConverter::appendRecordCopy(const Expr *Source, const VarDecl *Target, const auto *DRE = dyn_cast(Source); const auto *SourceVar = DRE ? dyn_cast(DRE->getDecl()) : nullptr; const RecordDecl *TargetRecord = getRecordFromType(Target->getType()); - // Copying out of a promoted object reads each leaf from its storage; the - // promoted source has no flattened companion to read instead. - if (promotedRootLocal(Source) && Target->isLocalVarDeclOrParm() && - TargetRecord && TargetRecord->getDefinition() && + // Copying out of a record kept in memory, a local object or one a + // pointer or reference addresses, reads each field where it is. + if (Target->isLocalVarDeclOrParm() && TargetRecord && + TargetRecord->getDefinition() && Ctx.hasSameUnqualifiedType(Target->getType(), Source->getType())) { - auto SourcePlace = objectPlace(Source); - if (!SourcePlace) - return true; - if (auto AccessCondition = SourcePlace->takeAccessCondition()) - Out.push_back(std::make_unique( - std::move(AccessCondition), Loc, ProofObligationKind::Bounds)); - std::unique_ptr SourceBase = SourcePlace->takeAddress(); - for (const FieldDecl *Field : TargetRecord->getDefinition()->fields()) { - auto FieldOffset = recordFieldOffset(Field); - VType FieldType = VType::fromQualType(Field->getType(), IntMode, Ctx); - if (!FieldOffset || FieldType.isAggregate() || - FieldType.Kind == VTypeKind::Unsupported) { - error(CurrentFn->Name + - ": unsupported aggregate copy out of an automatic " - "object"); - return true; + std::vector>> Fields; + if (recordFieldsInMemory(Source, Loc, Fields)) { + for (auto &[Field, Value] : Fields) { + Out.push_back(std::make_unique( + valueName(Target) + "." + Field->getNameAsString(), + std::move(Value), Loc)); + markInitialized(Target, Field); } - Out.push_back(std::make_unique( - valueName(Target) + "." + Field->getNameAsString(), - std::make_unique( - objectLeafAddress(SourceBase.get(), *FieldOffset, Loc), FieldType, - Loc), - Loc)); - markInitialized(Target, Field); + return true; } - return true; } const RecordDecl *SourceRecord = SourceVar ? getRecordFromType(SourceVar->getType()) : nullptr; @@ -6484,12 +6726,98 @@ bool ASTConverter::appendObjectCopy(const Expr *Source, QualType Ty, return true; } +bool ASTConverter::appendMemberInitializers( + const CXXConstructorDecl *Ctor, const VExpr *Base, uint64_t Offset, + SourceLocation Loc, std::vector> &Out) { + for (const CXXCtorInitializer *Init : Ctor->inits()) { + const FieldDecl *Field = Init->getMember(); + auto FieldOffset = Field ? recordFieldOffset(Field) : std::nullopt; + if (!FieldOffset) { + error(CurrentFn->Name + ": unsupported constructor initializer"); + return false; + } + const SourceLocation At = + Init->isWritten() ? Init->getSourceLocation() : Loc; + if (!appendObjectInitialization(Init->getInit(), Field->getType(), Base, + Offset + *FieldOffset, At, Out)) + return false; + } + return true; +} + +bool ASTConverter::appendConstruction( + const CXXConstructExpr *Construct, QualType Ty, const VExpr *Base, + uint64_t Offset, SourceLocation Loc, + std::vector> &Out) { + const CXXConstructorDecl *Ctor = Construct->getConstructor(); + if (!Ctor || Ty->isArrayType() || !Ty->getAsCXXRecordDecl()) { + error(CurrentFn->Name + + ": arrays of objects with constructors are not supported yet"); + return false; + } + if (auto Reason = unsupportedConstructor(Ctor)) { + error(CurrentFn->Name + ": " + Ctor->getQualifiedNameAsString() + ": " + + *Reason); + return false; + } + // An implicit or defaulted default constructor initializes each member as + // its declaration says, which is all it does. + if (!Ctor->isUserProvided()) { + if (!Ctor->isDefaultConstructor()) { + error(CurrentFn->Name + ": unsupported constructor initialization of an " + "automatic object"); + return false; + } + if (Construct->requiresZeroInitialization() && + !appendObjectZeroInitialization(Ty, Base, Offset, Loc, Out)) + return false; + const auto *Definition = + dyn_cast_or_null(Ctor->getDefinition()); + return appendMemberInitializers(Definition ? Definition : Ctor, Base, + Offset, Loc, Out); + } + // A constructor the class provides is a call, passing the object's + // address as `this`. + if (!functionContract(Ctor)) { + error(CurrentFn->Name + + ": call to function without a verification " + "contract: " + + Ctor->getQualifiedNameAsString()); + return false; + } + std::vector> Args; + Args.push_back(objectLeafAddress(Base, Offset, Loc)); + for (unsigned I = 0; I < Construct->getNumArgs(); ++I) { + const ParmVarDecl *Formal = + I < Ctor->getNumParams() ? Ctor->getParamDecl(I) : nullptr; + if (Formal && isFlattenedRecordType(Formal->getType())) { + if (!appendRecordCallArgument(Construct->getArg(I), Formal, Args)) + return false; + continue; + } + std::unique_ptr Arg; + convertExecCallArg(Construct->getArg(I), Formal, Out, Arg); + if (!Arg) + return false; + Args.push_back(std::move(Arg)); + } + Out.push_back(std::make_unique(Ctor->getNameAsString(), + functionIdentity(Ctor), + std::move(Args), "", Loc, false)); + return true; +} + bool ASTConverter::appendObjectInitialization( const Expr *Init, QualType Ty, const VExpr *Base, uint64_t Offset, SourceLocation Loc, std::vector> &Out) { if (!Init) return true; Init = Init->IgnoreParens(); + if (const auto *Default = dyn_cast(Init)) + return appendObjectInitialization(Default->getExpr(), Ty, Base, Offset, Loc, + Out); + if (const CXXConstructExpr *Construct = constructionOf(Init)) + Init = Construct; if (const auto *Cast = dyn_cast(Init); Cast && Cast->getCastKind() == CK_NoOp) Init = Cast->getSubExpr()->IgnoreParens(); @@ -6503,14 +6831,13 @@ bool ASTConverter::appendObjectInitialization( return true; return appendObjectZeroInitialization(Ty, Base, Offset, Loc, Out); } - if (Construct->getNumArgs() == 1 && Ctor && - (Ctor->isCopyConstructor() || Ctor->isMoveConstructor())) { + // An implicit or defaulted copy copies the members; one the class + // provides runs its body. + if (Construct->getNumArgs() == 1 && Ctor && !Ctor->isUserProvided() && + (Ctor->isCopyConstructor() || Ctor->isMoveConstructor())) Init = Construct->getArg(0)->IgnoreParens(); - } else { - error(CurrentFn->Name + ": unsupported constructor initialization of an " - "automatic object"); - return false; - } + else + return appendConstruction(Construct, Ty, Base, Offset, Loc, Out); } if (isa(Init) || isa(Init)) return appendObjectZeroInitialization(Ty, Base, Offset, Loc, Out); @@ -6771,6 +7098,26 @@ ASTConverter::convertStmtBody(const Stmt *S) { } } if (CurrentFn->ReturnType.Kind == VTypeKind::Struct) { + // A record kept in memory is returned as its fields, read before + // the lifetimes of the locals end. + std::vector>> + Fields; + if (auto InMemory = + recordFieldsInMemory(RetE, RS->getBeginLoc(), Fields)) { + if (!*InMemory) + return Out; + const std::string Tmp = + "__aggregate_return_" + std::to_string(++NestedCallId); + for (auto &[Field, Value] : Fields) + Out.push_back(std::make_unique( + Tmp + "." + Field->getNameAsString(), std::move(Value), + RS->getBeginLoc())); + appendReturn(std::make_unique(Tmp, CurrentFn->ReturnType, + RS->getBeginLoc()), + Out, RS->getBeginLoc()); + InitializationPathReachable = false; + return Out; + } auto RecordValue = convertExpr(RetE); if (!RecordValue) return Out; diff --git a/clang/lib/Verify/Frontend/ASTConverter.h b/clang/lib/Verify/Frontend/ASTConverter.h index b4695a0f3a..ba82b77b06 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.h +++ b/clang/lib/Verify/Frontend/ASTConverter.h @@ -89,6 +89,9 @@ class ASTConverter { /// address parameter, by the synthetic parameter of the field's entry value /// (VFunction::FieldParams). std::map FieldExtentParameters; + /// Converting a clause where an extent marker states nothing (a class + /// invariant at exit): each marker is true. + bool DropExtentMarkers = false; std::set GhostLocals; unsigned DynamicProvenanceId = 0; unsigned DynamicPointerAssignmentId = 0; @@ -231,6 +234,18 @@ class ASTConverter { const VExpr *Base, uint64_t Offset, SourceLocation Loc, std::vector> &Out); + /// The member initializers of a constructor, in the order they run, on + /// the object at Base + Offset. + bool appendMemberInitializers(const CXXConstructorDecl *Ctor, + const VExpr *Base, uint64_t Offset, + SourceLocation Loc, + std::vector> &Out); + /// Runs a constructor on the object at Base + Offset: a call of one the + /// class provides, else its members' initializers. + bool appendConstruction(const CXXConstructExpr *Construct, QualType Ty, + const VExpr *Base, uint64_t Offset, + SourceLocation Loc, + std::vector> &Out); bool appendObjectZeroInitialization(QualType Ty, const VExpr *Base, uint64_t Offset, SourceLocation Loc, std::vector> &Out); @@ -286,6 +301,13 @@ class ASTConverter { std::string Provenance = ""); bool appendRecordCallArgument(const Expr *E, const ParmVarDecl *Formal, std::vector> &Args); + /// The fields of a record value that is kept in memory, a local object or + /// one a pointer or reference addresses, each read where it is: nothing + /// when E is no such record, false after an error. + std::optional recordFieldsInMemory( + const Expr *E, SourceLocation Loc, + std::vector>> + &Fields); std::unique_ptr convertAssignmentValue(const BinaryOperator *Assignment); void appendAssignment(const Expr *LHS, std::unique_ptr Value, @@ -351,8 +373,13 @@ class ASTConverter { /// of FCI's preconditions names a synthetic parameter for its entry value /// (VFunction::FieldParams), and returns them for the default /// separation. - std::vector collectFieldExtents(const FunctionContractInfo &FCI, - VFunction &Fn); + std::vector + collectFieldExtents(const FunctionContractInfo &FCI, + llvm::ArrayRef Invariants, VFunction &Fn); + std::vector entryClassInvariants(const CXXMethodDecl *Method, + bool Constructor) const; + std::vector exitClassInvariants(const CXXMethodDecl *Method, + bool Constructor) const; void registerLayoutType(QualType QT, VFunction &Fn); void buildRecordLayout(QualType QT, VFunction &Fn); void buildArrayLayout(QualType QT, const ConstantArrayType *CAT, diff --git a/clang/lib/Verify/IR/VStmt.cpp b/clang/lib/Verify/IR/VStmt.cpp index be8f995c66..8ec2bd2f14 100644 --- a/clang/lib/Verify/IR/VStmt.cpp +++ b/clang/lib/Verify/IR/VStmt.cpp @@ -199,6 +199,7 @@ VFunction verify::cloneVFunction(const VFunction &Fn) { Out.SourceVariables = Fn.SourceVariables; Out.ScalarReferenceParams = Fn.ScalarReferenceParams; Out.RecordParams = Fn.RecordParams; + Out.IsConstructor = Fn.IsConstructor; for (const auto &[Name, Field] : Fn.FieldParams) Out.FieldParams.emplace_back(Name, cloneVExpr(Field.get())); Out.ConstAddressParams = Fn.ConstAddressParams; diff --git a/clang/lib/Verify/IR/VStmt.h b/clang/lib/Verify/IR/VStmt.h index 380b5f31b5..dcdd0badfa 100644 --- a/clang/lib/Verify/IR/VStmt.h +++ b/clang/lib/Verify/IR/VStmt.h @@ -345,6 +345,9 @@ struct VFunction { /// [[cppverify::trusted]]: its contract is assumed and its body, if any, /// is not verified. bool IsTrusted = false; + /// A constructor: its object's lifetime begins at `this`, uninitialized, + /// and the body initializes every leaf of it. + bool IsConstructor = false; /// The declaration, for diagnostics about the function itself. SourceLocation DeclLoc; bool NeedsDecreasesCheck = false; diff --git a/clang/lib/Verify/Transform/LoopUnroll.cpp b/clang/lib/Verify/Transform/LoopUnroll.cpp index ea32b88502..cdb9564651 100644 --- a/clang/lib/Verify/Transform/LoopUnroll.cpp +++ b/clang/lib/Verify/Transform/LoopUnroll.cpp @@ -257,6 +257,7 @@ VFunction LoopUnroller::unroll(const VFunction &Fn, unsigned K) { Out.SourceVariables = Fn.SourceVariables; Out.ScalarReferenceParams = Fn.ScalarReferenceParams; Out.RecordParams = Fn.RecordParams; + Out.IsConstructor = Fn.IsConstructor; for (const auto &[Name, Field] : Fn.FieldParams) Out.FieldParams.emplace_back(Name, cloneVExpr(Field.get())); Out.ConstAddressParams = Fn.ConstAddressParams; diff --git a/clang/lib/Verify/Transform/Passivize.cpp b/clang/lib/Verify/Transform/Passivize.cpp index 668f007ed4..659e59d04d 100644 --- a/clang/lib/Verify/Transform/Passivize.cpp +++ b/clang/lib/Verify/Transform/Passivize.cpp @@ -2927,6 +2927,119 @@ applicationKey(const VSpecCallExpr &C, return true; } +/// Every scalar leaf of a layout at its offset, its array repetitions +/// expanded; nothing when there are more than Limit. +static std::optional>> +expandedLeaves(const VObjectLayout &Layout, size_t Limit) { + std::vector> Out; + for (const VObjectLeaf &Leaf : Layout.Leaves) { + std::vector Offsets = {Leaf.OffsetBytes}; + for (const VObjectRepeat &Repeat : Leaf.Repeats) { + std::vector Next; + for (uint64_t Start : Offsets) + for (uint64_t K = 0; K < Repeat.Count; ++K) { + if (Out.size() + Next.size() >= Limit) + return std::nullopt; + Next.push_back(Start + K * Repeat.StrideBytes); + } + Offsets = std::move(Next); + } + for (uint64_t Offset : Offsets) { + if (Out.size() >= Limit) + return std::nullopt; + Out.push_back({Offset, &Leaf}); + } + } + return Out; +} + +/// The layout of the object a constructor constructs. +static const VObjectLayout *constructedLayout(const VFunction &Fn) { + auto Identity = Fn.RecordParams.find("this"); + if (!Fn.IsConstructor || Identity == Fn.RecordParams.end()) + return nullptr; + auto Layout = llvm::find_if(Fn.Layouts, [&](const VObjectLayout &L) { + return L.TypeIdentity == Identity->second; + }); + return Layout == Fn.Layouts.end() ? nullptr : &*Layout; +} + +/// The condition a definedness check asks for, without the guards it holds +/// under: `!g || c` as built by makeImplies, and the range of a quantified +/// check. +static const VExpr *checkedCondition(const VExpr *E) { + while (E) { + if (E->K == VExpr::BinOp) { + const auto *B = static_cast(E); + if (B->Op == VBinOp::Or && B->Lhs->K == VExpr::UnaryOp && + static_cast(B->Lhs.get())->Op == + VUnaryOp::Not) { + E = B->Rhs.get(); + continue; + } + } + if (E->K == VExpr::Forall) { + E = static_cast(E)->Body.get(); + continue; + } + return E; + } + return E; +} + +/// Whether \p E may have another value at a loop's head than before the +/// loop: it reads a variable, a field, or a heap the loop modifies, outside +/// cppverify::old, which reads the entry state. +static bool readsLoopState(const VExpr *E, + const std::set &Modified) { + if (!E) + return false; + switch (E->K) { + case VExpr::Old: + return false; + case VExpr::Var: { + const auto *V = static_cast(E); + return Modified.count(V->Name) || Modified.count(V->ProvenanceVariable); + } + case VExpr::FieldAccess: { + const auto *F = static_cast(E); + if (F->Base->K == VExpr::Var) { + const std::string Prefix = + static_cast(F->Base.get())->Name + "."; + for (const std::string &Name : Modified) + if (llvm::StringRef(Name).starts_with(Prefix)) + return true; + } + break; + } + case VExpr::Load: + if (Modified.count(VHeapName)) + return true; + break; + case VExpr::SpecCall: + if (static_cast(E)->ReadsHeap && + Modified.count(VHeapName)) + return true; + break; + case VExpr::UnaryOp: { + const auto *U = static_cast(E); + if ((U->Op == VUnaryOp::ValidPtr && (Modified.count(VAllocationHeapName) || + Modified.count(VLivenessHeapName))) || + (U->Op == VUnaryOp::InitializedPtr && + Modified.count(VInitializationHeapName))) + return true; + break; + } + default: + break; + } + bool Found = false; + forEachVExprChild(E, [&](const VExpr *Child) { + Found = Found || readsLoopState(Child, Modified); + }); + return Found; +} + /// Whether \p E mentions the variable \p Name free. static bool mentionsFree(const VExpr *E, const std::string &Name) { if (!E) @@ -3441,6 +3554,9 @@ class PassivizerImpl { /// parameter without one. std::vector OriginObjects; std::set RepresentedAllocationPointers; + /// The type and size of the object each of those pointers was defined to + /// address. + std::map> RepresentedObjects; std::vector StoredPointerCells; std::set HeapBases; std::set HeapVariables; @@ -3814,19 +3930,93 @@ class PassivizerImpl { return true; } + /// The one cell a store through \p Address writes, when the address is a + /// pointer into local or dynamic storage (a reference to a local, say) that + /// the loop assigns neither nor its lifetime companion. + std::optional + representedCell(const VExpr *Address, const VType &CellType, + const std::map &Renames, + const std::set &Assigned, SourceLocation Loc) { + while (Address && Address->K == VExpr::Cast) + Address = static_cast(Address)->Inner.get(); + if (!Address || Address->K != VExpr::Var) + return std::nullopt; + const auto *Pointer = static_cast(Address); + if (Pointer->ProvenanceVariable.empty() || Assigned.count(Pointer->Name) || + Assigned.count(Pointer->ProvenanceVariable)) + return std::nullopt; + CloneCtx Ctx{Renames, OldState, false}; + auto Cell = cloneExpr(Address, Ctx); + return cellRegion(Cell.get(), CellType, Loc); + } + + /// The local or dynamic object that the pointer its allocation defined + /// addresses, when the loop assigns neither the pointer nor its lifetime + /// companion: every access through it lies in the object, at a field of + /// its layout and an index its fixed array bounds (a dynamic object is one + /// scalar). The object is its scalar leaves, each one cell, so the loop's + /// frame stays a chain of stores; without a layout it is its bytes. + bool representedRegions(const VExpr *Root, + const std::map &Renames, + const std::set &Assigned, + SourceLocation Loc, std::vector &Out) { + if (!Root || Root->K != VExpr::Var) + return false; + const auto *Pointer = static_cast(Root); + auto Object = RepresentedObjects.find(Pointer->Name); + if (Object == RepresentedObjects.end() || + Pointer->ProvenanceVariable.empty() || Assigned.count(Pointer->Name) || + Assigned.count(Pointer->ProvenanceVariable)) + return false; + const auto &[Type, Bytes] = Object->second; + CloneCtx Ctx{Renames, OldState, false}; + auto Base = cloneExpr(Root, Ctx); + auto At = [&](uint64_t Offset) { + return addBytes(cloneVExpr(Base.get()), + std::make_unique(std::to_string(Offset), + pointerOffsetType(), Loc), + Loc); + }; + if (Type.isInt() || Type.Kind == VTypeKind::Bool || + Type.Kind == VTypeKind::Ptr) { + Out.push_back(cellRegion(Base.get(), Type, Loc)); + return true; + } + const auto Layout = llvm::find_if(Fn.Layouts, [&](const VObjectLayout &L) { + return L.TypeIdentity == Type.TypeIdentity; + }); + if (Layout != Fn.Layouts.end() && Layout->SizeBytes == Bytes) + if (auto Leaves = expandedLeaves(*Layout, Bytes); + Leaves && !Leaves->empty()) { + for (const auto &[Offset, Leaf] : *Leaves) + Out.push_back(cellRegion(At(Offset).get(), Leaf->Ty, Loc)); + return true; + } + Out.push_back( + Region{cloneVExpr(Base.get()), At(std::max(Bytes, 1))}); + return true; + } + bool loopWriteRegions(const std::vector> &Stmts, const std::map &Renames, + const std::set &Assigned, std::vector &Out) { for (const auto &S : Stmts) { switch (S->K) { case VStmt::Store: { const auto &St = static_cast(*S); auto R = parameterCell(St.Ptr.get(), St.Value->Ty, Renames, St.Loc); + if (!R) + R = representedCell(St.Ptr.get(), St.Value->Ty, Renames, Assigned, + St.Loc); if (!R && originRegions(addressRoot(St.Ptr.get()), Renames, St.Loc, Out)) break; if (!R) R = rootRegion(addressRoot(St.Ptr.get()), Renames, St.Loc); + if (!R && representedRegions(addressRoot(St.Ptr.get()), Renames, + Assigned, St.Loc, Out)) + break; if (!R) return false; Out.push_back(std::move(*R)); @@ -3877,14 +4067,22 @@ class PassivizerImpl { [&](const VValidExtent &Extent) { return Extent.Base == Param; }))); - if (OneCell) - if (auto Cell = parameterCell(Actual, Target->Ty, Renames, C.Loc)) { + if (OneCell) { + auto Cell = parameterCell(Actual, Target->Ty, Renames, C.Loc); + if (!Cell) + Cell = + representedCell(Actual, Target->Ty, Renames, Assigned, C.Loc); + if (Cell) { Out.push_back(std::move(*Cell)); continue; } + } if (originRegions(addressRoot(Actual), Renames, C.Loc, Out)) continue; auto R = rootRegion(addressRoot(Actual), Renames, C.Loc); + if (!R && representedRegions(addressRoot(Actual), Renames, Assigned, + C.Loc, Out)) + continue; if (!R) return false; Out.push_back(std::move(*R)); @@ -3896,19 +4094,19 @@ class PassivizerImpl { return false; case VStmt::If: { const auto &I = static_cast(*S); - if (!loopWriteRegions(I.Then, Renames, Out) || - !loopWriteRegions(I.Else, Renames, Out)) + if (!loopWriteRegions(I.Then, Renames, Assigned, Out) || + !loopWriteRegions(I.Else, Renames, Assigned, Out)) return false; break; } case VStmt::While: - if (!loopWriteRegions(static_cast(*S).Body, - Renames, Out)) + if (!loopWriteRegions(static_cast(*S).Body, Renames, + Assigned, Out)) return false; break; case VStmt::Seq: - if (!loopWriteRegions(static_cast(*S).Stmts, - Renames, Out)) + if (!loopWriteRegions(static_cast(*S).Stmts, Renames, + Assigned, Out)) return false; break; default: @@ -4292,6 +4490,57 @@ class PassivizerImpl { P.ResultVarName = ResultName; } + /// Whether S starts a lifetime, whose storage is then uninitialized. + static bool startsLifetime(const VStmt &S) { + switch (S.K) { + case VStmt::Allocate: + return true; + case VStmt::If: { + const auto &I = static_cast(S); + return llvm::any_of(I.Then, + [](const auto &T) { return startsLifetime(*T); }) || + llvm::any_of(I.Else, + [](const auto &E) { return startsLifetime(*E); }); + } + case VStmt::While: + return llvm::any_of(static_cast(S).Body, + [](const auto &B) { return startsLifetime(*B); }); + case VStmt::GhostBlock: + return llvm::any_of(static_cast(S).Body, + [](const auto &B) { return startsLifetime(*B); }); + case VStmt::Seq: + return llvm::any_of(static_cast(S).Stmts, + [](const auto &B) { return startsLifetime(*B); }); + default: + return false; + } + } + + /// `forall a. initialized_before[a] -> initialized_after[a]`, triggered by + /// reads of the later state. + static std::unique_ptr initializationKept(const std::string &Before, + const std::string &After, + SourceLocation Loc) { + const std::string Binder = "__init_address"; + auto Address = [&] { + return std::make_unique( + VBinOp::Add, std::make_unique(0, VType::makePtr(), Loc), + std::make_unique(Binder, VType::makeInt32(VIntMode::Math), + Loc), + VType::makePtr(), Loc); + }; + auto WasInitialized = + std::make_unique(Address(), VType::makeBool(), Loc, Before); + auto IsInitialized = std::make_unique( + std::make_unique(Address(), VType::makeBool(), Loc, After), + VType::makeBool(), VType::makeBool(), Loc, /*IsTrigger=*/true); + return std::make_unique( + Binder, nullptr, nullptr, + makeOr(makeNot(std::move(WasInitialized), Loc), + std::move(IsInitialized), Loc), + Loc, VType::makeInt32(VIntMode::Math)); + } + void collectModified(const VStmt &S, std::set &Out) const { switch (S.K) { case VStmt::Assign: @@ -4299,6 +4548,9 @@ class PassivizerImpl { break; case VStmt::Store: Out.insert(VHeapName); + // A store to local or dynamic storage initializes the cell. + if (hasPointerProvenance(static_cast(S).Ptr.get())) + Out.insert(VInitializationHeapName); break; case VStmt::Allocate: { const auto &A = static_cast(S); @@ -4405,12 +4657,10 @@ class PassivizerImpl { /// A contract expression's memory checks, recorded before spec inlining, /// join its other checks, one obligation per kind. - void emitExprSafety(PassiveProgram &P, const VExpr *E, const VExpr *Guard, - SourceLocation Loc, - const std::map &Renames, - bool BridgeMachineValue = false, - const VExpr *SafetySource = nullptr, - const std::vector *MemoryChecks = nullptr) { + /// The definedness checks of E, or of SafetySource, the clause as written + /// that E instantiates, with the memory checks recorded for it. + SafetyChecks exprSafetyChecks(const VExpr *E, const VExpr *SafetySource, + const std::vector *MemoryChecks) { SafetyChecks Checks; collectSafety( SafetySource ? SafetySource : E, &FnMap, @@ -4420,6 +4670,16 @@ class PassivizerImpl { if (MemoryChecks && !Fn.TotalExpressions) for (const VMemoryCheck &Check : *MemoryChecks) Checks.push_back({Check.Kind, cloneVExpr(Check.Cond.get())}); + return Checks; + } + + void emitExprSafety(PassiveProgram &P, const VExpr *E, const VExpr *Guard, + SourceLocation Loc, + const std::map &Renames, + bool BridgeMachineValue = false, + const VExpr *SafetySource = nullptr, + const std::vector *MemoryChecks = nullptr) { + SafetyChecks Checks = exprSafetyChecks(E, SafetySource, MemoryChecks); groupByKind(Checks); CloneCtx Ctx{Renames, OldState, false}; for (const SafetyCheck &Check : Checks) @@ -4428,6 +4688,26 @@ class PassivizerImpl { emitMathBridge(P, E, Guard, Loc, BridgeMachineValue); } + /// The definedness of an invariant, assumed at its loop's head: every + /// path into the head (entry, the end of an iteration, a continue) asserts + /// it with the invariant, so at the head it holds by the same induction, + /// and the reads it makes, of memory written in the loop included, are + /// initialized and in bounds there. A check whose condition reads nothing + /// the loop modifies is left out: what it asks for holds at the head as it + /// did before the loop, and its guards alone, of state the loop changes, + /// are what an invariant states itself. + void assumeInvariantSafety(PassiveProgram &P, const VWhileStmt &W, + const VExpr *Inv, const VExpr *Guard, + const std::map &Renames, + const std::set &Modified) { + CloneCtx Ctx{Renames, OldState, false}; + for (const SafetyCheck &Check : + exprSafetyChecks(Inv, Inv, invariantChecks(W, Inv))) + if (readsLoopState(checkedCondition(Check.Cond.get()), Modified)) + emitPassive(P, PassiveStmt::Assume, cloneExpr(Check.Cond.get(), Ctx), + Guard, Inv->Loc); + } + void emitMathBridge(PassiveProgram &P, const VExpr *E, const VExpr *Guard, SourceLocation Loc, bool BridgeMachineValue = false) { llvm::SaveAndRestore Exact(Origin, "exact"); @@ -4478,6 +4758,8 @@ class PassivizerImpl { OwnedAllocationIdentities.push_back(ProvenanceName.str()); RepresentedAllocationPointers.insert(ResultTarget.str()); + RepresentedObjects[ResultTarget.str()] = {Summary.AllocatedType, + Summary.SizeBytes}; auto NonzeroProvenance = std::make_unique( VBinOp::Ne, cloneVExpr(Provenance.get()), std::make_unique(0, VType::makePtr(), Loc), @@ -4812,6 +5094,37 @@ class PassivizerImpl { return Renames; } + /// A constructor's object at its end: every leaf initialized, each a check + /// at its member's declaration. + void + emitConstructedChecks(PassiveProgram &P, + const std::map &Renames) { + const VObjectLayout *Layout = constructedLayout(Fn); + auto Leaves = Layout ? expandedLeaves(*Layout, 4096) : std::nullopt; + if (!Leaves) { + P.ExitAsserts.push_back({ProofObligationKind::Unsupported, + makeBoolLiteral(false, Fn.DeclLoc), + "a constructor whose object has no known " + "layout"}); + return; + } + CloneCtx Ctx{Renames, OldState, false}; + for (const auto &[Offset, Leaf] : *Leaves) { + const SourceLocation At = Leaf->Loc.isValid() ? Leaf->Loc : Fn.DeclLoc; + VVarExpr This("this", VType::makePtr(), At); + P.ExitAsserts.push_back( + {ProofObligationKind::Initialization, + std::make_unique( + VUnaryOp::InitializedPtr, + addBytes(cloneExpr(&This, Ctx), + std::make_unique(std::to_string(Offset), + pointerOffsetType(), At), + At), + VType::makeBool(), At, "", "", + stateHeapName(Ctx, VInitializationHeapName, ""))}); + } + } + PassiveProgram run() { PassiveProgram P; P.FunctionName = Fn.Name; @@ -4842,6 +5155,8 @@ class PassivizerImpl { if (OfParameter) PostRenames[Name] = static_cast(*Entry).Name; } + if (Fn.IsConstructor) + emitConstructedChecks(P, Renames); // Postconditions are evaluated in order: a clause is evaluated where the // clauses before it hold. std::unique_ptr EarlierPosts; @@ -5133,6 +5448,9 @@ class PassivizerImpl { stateHeapName(Ctx, VAllocationHeapName, ""), stateHeapName(Ctx, VLivenessHeapName, "")), nullptr, Loc, ProofObligationKind::PointerValidity); + // A constructor's object is what it initializes. + if (Callee.IsConstructor && Name == "this") + continue; std::vector Leaves; for (const VObjectLeaf &Leaf : Layout->Leaves) { std::vector Offsets = {Leaf.OffsetBytes}; @@ -5206,7 +5524,50 @@ class PassivizerImpl { bool CanFrameRegions = Fn.ObjectModel && Callee.ObjectModel && !CanFrameExactly && !ActualModifies.empty() && !HasImplicitHeapEffect; + // The object of a record parameter is its leaves, each one cell, so the + // frame stays a chain of stores: the callee's stores are at its leaves. + auto RecordCells = [&](size_t I) -> std::optional> { + if (!InRecordParam(I) || + !isRegionFootprint(Callee.Modifies[I], + Callee.ScalarReferenceParams) || + !ActualModifies[I] || ActualModifies[I]->K != VExpr::Load || + ActualCounts[I]) + return std::nullopt; + const auto *Root = static_cast(addressRoot( + static_cast(Callee.Modifies[I].Target.get()) + ->Ptr.get())); + if (llvm::any_of(Callee.ValidExtents, [&](const VValidExtent &Extent) { + return Extent.Base == Root->Name; + })) + return std::nullopt; + const std::string &Identity = Callee.RecordParams.at(Root->Name); + auto Layout = llvm::find_if(Callee.Layouts, [&](const VObjectLayout &L) { + return L.TypeIdentity == Identity; + }); + if (Layout == Callee.Layouts.end()) + return std::nullopt; + auto Leaves = expandedLeaves(*Layout, 4096); + if (!Leaves || Leaves->empty()) + return std::nullopt; + const VExpr *Object = + static_cast(ActualModifies[I].get())->Ptr.get(); + std::vector Cells; + for (const auto &[Offset, Leaf] : *Leaves) { + auto Address = + addBytes(cloneVExpr(Object), + std::make_unique(std::to_string(Offset), + pointerOffsetType(), Loc), + Loc); + Cells.push_back(cellRegion(Address.get(), Leaf->Ty, Loc)); + } + return Cells; + }; for (size_t I = 0; CanFrameRegions && I < ActualModifies.size(); ++I) { + if (auto Cells = RecordCells(I)) { + for (Region &Cell : *Cells) + CallRegions.push_back(std::move(Cell)); + continue; + } std::optional Bytes; if (ActualModifies[I] && ActualModifies[I]->K == VExpr::Load && (!hasPointerProvenance( @@ -5750,6 +6111,26 @@ class PassivizerImpl { havocFootprints(P, Renames, *Callee, ActualModifies, ActualCounts, ParamMap, Ctx, EntryHeap, HasImplicitHeapEffect, C.Loc); + // A constructor initializes every leaf of its object, as its exit checks + // show, so the caller's storage holds an initialized object after it. + if (Callee->IsConstructor) { + const VObjectLayout *Layout = constructedLayout(*Callee); + auto Leaves = Layout ? expandedLeaves(*Layout, 4096) : std::nullopt; + auto This = ParamMap.find("this"); + if (!Leaves || This == ParamMap.end()) + emitPassive(P, PassiveStmt::Assert, makeBoolLiteral(false, C.Loc), + nullptr, C.Loc, ProofObligationKind::Unsupported, + "a constructor whose object has no known layout"); + else + for (const auto &[Offset, Leaf] : *Leaves) + updateHeap( + P, Renames, VInitializationHeapName, + addBytes(cloneVExpr(This->second.get()), + std::make_unique( + std::to_string(Offset), pointerOffsetType(), C.Loc), + C.Loc), + makeBoolLiteral(true, C.Loc), nullptr, C.Loc); + } std::map> PostParamMap; for (const auto &[Name, Value] : ParamMap) @@ -6163,6 +6544,7 @@ class PassivizerImpl { } PointerValueVariables.insert(A.Target); RepresentedAllocationPointers.insert(A.Target); + RepresentedObjects[A.Target] = {A.AllocatedType, A.SizeBytes}; const std::string AllocationBefore = Renames[VAllocationHeapName]; const std::string LivenessBefore = Renames[VLivenessHeapName]; @@ -6436,11 +6818,13 @@ class PassivizerImpl { std::set Modified; for (const auto &Body : W.Body) collectModified(*Body, Modified); + const bool StartsLifetime = llvm::any_of( + W.Body, [](const auto &Body) { return startsLifetime(*Body); }); // A loop in the object model writes only the objects its stores and // calls reach; the rest of the heap keeps its values. std::vector WriteRegions; bool Framed = Fn.ObjectModel && Modified.count(VHeapName) && - loopWriteRegions(W.Body, Renames, WriteRegions); + loopWriteRegions(W.Body, Renames, Modified, WriteRegions); // Every store and call in the loop is checked against the function's // own frame, so that frame bounds what the loop writes too; with both, // only cells in both may change. @@ -6468,6 +6852,12 @@ class PassivizerImpl { Renames[Name] = HeadName; emitInactiveFrame(P, PreviousName, HeadName, typeForName(Name), Enters.get(), W.Loc); + // Without a lifetime starting in it, a loop only initializes + // storage: what was initialized before it still is at its head. + if (Name == VInitializationHeapName && !StartsLifetime) + emitPassive(P, PassiveStmt::Assume, + initializationKept(PreviousName, HeadName, W.Loc), + Active.get(), W.Loc); if (Framed && Name == VHeapName) { const bool OnlyCells = !WriteRegions.empty() && @@ -6515,6 +6905,7 @@ class PassivizerImpl { } Origin = "inv"; for (const auto &Inv : W.Invariants) { + assumeInvariantSafety(P, W, Inv.get(), Active.get(), Renames, Modified); auto BoundInv = cloneExpr(Inv.get(), HeadCtx); emitPassive(P, PassiveStmt::Assume, std::move(BoundInv), Active.get(), W.Loc); diff --git a/clang/test/Verify/suite/class_invariants.cpp b/clang/test/Verify/suite/class_invariants.cpp new file mode 100644 index 0000000000..293be0b1a2 --- /dev/null +++ b/clang/test/Verify/suite/class_invariants.cpp @@ -0,0 +1,237 @@ +// RUN: not %cpp-verify --jobs=1 %s -- > %t 2>&1 +// RUN: FileCheck %s < %t +// RUN: FileCheck %s --check-prefix=SOUND < %t +// +// A class invariant holds at the boundary of every public member function, +// which assumes it on entry and must restore it, and every constructor must +// establish it. It is checked at every call, internal calls included, so a +// private member function may work with it broken, and no call observes it +// broken. +// +// No proof here holds only because no execution reaches its end. +// SOUND-NOT: vacuous + +class Ring { +public: + Ring() + cppverify::post(head == 0 && count == 0) + : head(0), count(0) + { + for (int i = 0; i < 8; i = i + 1) + cppverify::invariant(0 <= i && i <= 8) + cppverify::invariant(head == 0 && count == 0) + cppverify::invariant(cppverify::forall(k, 0, i, buf[k] == 0)) + cppverify::decreases(8 - i) + { + buf[i] = 0; + } + } + + void push(int v) + cppverify::pre(count < 8) + cppverify::post(count == cppverify::old(count) + 1) + { + buf[(head + count) % 8] = v; + count = count + 1; + } + + int pop() + cppverify::pre(count > 0) + cppverify::post(count == cppverify::old(count) - 1) + { + int v = buf[head]; + head = (head + 1) % 8; + count = count - 1; + return v; + } + + int size() const + cppverify::post(cppverify::result == count) + { + return count; + } + + int front_index() const + cppverify::post(cppverify::result == head) + { + return head; + } + + // Breaks the invariant. + void skip() + cppverify::post(true) + { + head = 8; + } + + // Works with the invariant broken, then restores it. + void rotate() + cppverify::post(true) + { + set_head(9); + set_head(0); + } + + // Calls a public member function with the invariant broken. + int peek_broken() + cppverify::post(true) + { + set_head(9); + int n = size(); + set_head(0); + return n; + } + +private: + void set_head(int h) + cppverify::modifies(head) + cppverify::post(head == h) + { + head = h; + } + + int buf[8]; + int head; + int count; + +public: + cppverify::type_invariant(0 <= head && head < 8 && 0 <= count && count <= 8); +}; +// CHECK-DAG: Verified: Ring::Ring [backend=z3] +// CHECK-DAG: Verified: Ring::push [backend=z3] +// CHECK-DAG: Verified: Ring::pop [backend=z3] +// CHECK-DAG: Verified: Ring::size [backend=z3] +// CHECK-DAG: Verified: Ring::rotate [backend=z3] +// CHECK-DAG: Verified: Ring::set_head [backend=z3] +// CHECK-DAG: error: verification failed: Ring::skip [{{.*}}::type-invariant@ +// CHECK-DAG: error: verification failed: Ring::peek_broken [{{.*}}::type-invariant@ + +// A constructor that does not establish the invariant. +class Window { +public: + Window(int f) + cppverify::post(first == f) + : first(f) {} + + int first; + + cppverify::type_invariant(0 <= first && first < 100); +}; +// CHECK-DAG: error: verification failed: Window::Window [{{.*}}::type-invariant@ + +class Bounded { +public: + Bounded(int f) + cppverify::pre(0 <= f && f < 100) + cppverify::post(first == f) + : first(f) {} + + int get() const + cppverify::post(cppverify::result == first) + { + return first; + } + + int first; + + cppverify::type_invariant(0 <= first && first < 100); +}; +// CHECK-DAG: Verified: Bounded::Bounded [backend=z3] + +// A caller knows the invariant after construction and after every public +// call, and must establish it before every public call. +int known() + cppverify::post(0 <= cppverify::result && cppverify::result < 100) +{ + Bounded b(42); + int v = b.get(); + return v; +} +// CHECK-DAG: Verified: known [backend=z3] + +int ring_use() + cppverify::post(cppverify::result == 1) +{ + Ring r; + r.push(7); + int i = r.front_index(); + cppverify::check(0 <= i && i < 8); + int n = r.size(); + return n; +} +// CHECK-DAG: Verified: ring_use [backend=z3] + +// pop's contract does not say what it returns. +int ring_value() + cppverify::post(cppverify::result == 7) +{ + Ring r; + r.push(7); + int v = r.pop(); + return v; +} +// CHECK-DAG: error: verification failed: ring_value [{{.*}}::postcondition@ + +int broken_by_caller() + cppverify::post(true) +{ + Bounded b(1); + b.first = 500; + return b.get(); +} +// CHECK-DAG: error: verification failed: broken_by_caller [{{.*}}::type-invariant@[[@LINE-2]] + +// An extent in a class invariant: on entry `this->data` points to `len` +// elements, as a pointer field's extent in a precondition does. At exit the +// marker states nothing; the next call checks the extent from what its +// caller knows. +class View { +public: + View(const int *p, int n) + cppverify::pre(cppverify::valid(p, n) && 0 <= n && n < 1000) + cppverify::post(data == p && len == n) + : data(p), len(n) {} + + int first() const + cppverify::pre(len > 0) + cppverify::post(cppverify::result == data[0]) + { + return data[0]; + } + + void grow() + cppverify::pre(len < 999) + cppverify::modifies(len) + cppverify::post(len == cppverify::old(len) + 1) + { + len = len + 1; + } + + const int *data; + int len; + + cppverify::type_invariant(cppverify::valid(data, len) && len >= 0 && len < 1000); +}; +// CHECK-DAG: Verified: View::View [backend=z3] +// CHECK-DAG: Verified: View::first [backend=z3] +// CHECK-DAG: Verified: View::grow [backend=z3] + +int first_of(const int *p, int n) + cppverify::pre(cppverify::valid(p, n) && 0 < n && n < 1000) + cppverify::post(cppverify::result == p[0]) +{ + View v(p, n); + int x = v.first(); + return x; +} +// CHECK-DAG: Verified: first_of [backend=z3] + +int grown(const int *p, int n) + cppverify::pre(cppverify::valid(p, n) && 0 < n && n < 999) +{ + View v(p, n); + v.grow(); + int x = v.first(); + return x; +} +// CHECK-DAG: error: verification failed: grown [{{.*}}::bounds@[[@LINE-3]] diff --git a/clang/test/Verify/suite/constructors.cpp b/clang/test/Verify/suite/constructors.cpp new file mode 100644 index 0000000000..c33a1ed441 --- /dev/null +++ b/clang/test/Verify/suite/constructors.cpp @@ -0,0 +1,270 @@ +// RUN: not %cpp-verify --jobs=1 %s -- > %t 2>&1 +// RUN: FileCheck %s < %t +// RUN: FileCheck %s --check-prefix=SOUND < %t +// RUN: not %cpp-verify --jobs=1 --backend=bmc --unroll=9 %s -- 2>&1 \ +// RUN: | FileCheck %s --check-prefix=BMC +// +// A constructor runs on storage its caller allocated: its object is +// uninitialized when it is entered, its member initializers run first, in +// declaration order, and it must initialize every member by its end. The +// caller passes the object's address as `this` and holds an initialized +// object after the call. An implicit or defaulted default constructor +// initializes the members as their declarations say. +// +// No proof here holds only because no execution reaches its end. +// SOUND-NOT: vacuous + +struct Counter { + Counter() + cppverify::post(n == 0 && limit == 10) + : n(0), limit(10) {} + + Counter(int l) + cppverify::pre(l > 0) + cppverify::post(n == 0 && limit == l) + { + n = 0; + limit = l; + } + + void bump() + cppverify::pre(n < limit) + cppverify::modifies(n) + cppverify::post(n == cppverify::old(n) + 1) + { + n = n + 1; + } + + int n; + int limit; +}; +// CHECK-DAG: Verified: Counter::Counter [backend=z3] +// BMC-DAG: Verified: Counter::Counter [backend=bmc, bound=0] + +int made() + cppverify::post(cppverify::result == 16) +{ + Counter c; + Counter d(5); + Counter e{1}; + d.bump(); + return c.limit + d.limit + c.n + d.n + e.n; +} +// CHECK-DAG: Verified: made [backend=z3] +// BMC-DAG: Verified: made [backend=bmc, bound=0] + +// A conversion by the constructor, and a copy, which copies the members. +int converted() + cppverify::post(cppverify::result == 6) +{ + Counter f = Counter(3); + Counter g = f; + return f.limit + g.limit; +} +// CHECK-DAG: Verified: converted [backend=z3] + +// Construction writes only the object constructed. +int others_kept() + cppverify::post(cppverify::result == 6) +{ + int x = 1; + int &r = x; + Counter c(5); + return r + c.limit; +} +// CHECK-DAG: Verified: others_kept [backend=z3] + +// Every member must be initialized. +struct Partial { + Partial(int l) + cppverify::post(limit == l) + { + limit = l; + } + + int n; + int limit; +}; +// CHECK-DAG: error: verification failed: Partial::Partial [{{.*}}::initialization@[[@LINE-3]]:7] + +// Members are initialized in declaration order, whatever the order of the +// initializers: `n` reads `limit` before it is initialized. +struct Early { + Early() + cppverify::post(true) + : limit(0), n(limit) {} + + int n; + int limit; +}; +// CHECK-DAG: error: verification failed: Early::Early [{{.*}}::initialization@ + +// The in-class initializers of the members a constructor does not name run +// in their place. +struct Defaults { + Defaults() + cppverify::post(a == 1 && b == 2) + : b(2) {} + + int a = 1; + int b; +}; +// CHECK-DAG: Verified: Defaults::Defaults [backend=z3] + +// An implicit default constructor is its members' initializers. +struct Point { + int x = 3; + int y = 4; +}; + +int point_sum() + cppverify::post(cppverify::result == 7) +{ + Point p; + return p.x + p.y; +} +// CHECK-DAG: Verified: point_sum [backend=z3] + +// So is one whose member's class has an implicit one. +struct Holder { + Point p; + int z = 0; +}; + +int holder_sum() + cppverify::post(cppverify::result == 7) +{ + Holder h; + return h.p.x + h.p.y + h.z; +} +// CHECK-DAG: Verified: holder_sum [backend=z3] + +// A member function called on the object before every member is +// initialized reads it as initialized, which C++ does not require: such a +// call is construct.unsupported, as an out-parameter's is. +struct Resets { + Resets() + cppverify::post(v == 0) + { + reset(); + } + + void reset() + cppverify::modifies(v) + cppverify::post(v == 0) + { + v = 0; + } + + int v; +}; +// CHECK-DAG: Unresolved: Resets::Resets [backend=z3] [reason=construct.unsupported] + +// A loop initializes an array member, as an invariant states. +struct Ring { + Ring() + cppverify::post(head == 0 && count == 0) + cppverify::post(cppverify::forall(k, 0, 8, buf[k] == 0)) + : head(0), count(0) + { + for (int i = 0; i < 8; i = i + 1) + cppverify::invariant(0 <= i && i <= 8) + cppverify::invariant(head == 0 && count == 0) + cppverify::invariant(cppverify::forall(k, 0, i, buf[k] == 0)) + cppverify::decreases(8 - i) + { + buf[i] = 0; + } + } + + int buf[8]; + int head; + int count; +}; +// CHECK-DAG: Verified: Ring::Ring [backend=z3] + +// A loop writes only the object constructed: the source keeps its values. +struct Copy4 { + Copy4(const int *src) + cppverify::pre(cppverify::valid(src, 4)) + cppverify::post(cppverify::forall(k, 0, 4, buf[k] == cppverify::old(src[k]))) + { + for (int i = 0; i < 4; i = i + 1) + cppverify::invariant(0 <= i && i <= 4) + cppverify::invariant(cppverify::forall(k, 0, i, buf[k] == src[k])) + cppverify::decreases(4 - i) + { + buf[i] = src[i]; + } + } + + int buf[4]; +}; +// CHECK-DAG: Verified: Copy4::Copy4 [backend=z3] + +int ring_count() + cppverify::post(cppverify::result == 0) +{ + Ring r; + return r.count + r.buf[7]; +} +// CHECK-DAG: Verified: ring_count [backend=z3] + +// A constructor that writes another object states it. +struct Logged { + Logged(int *log) + cppverify::pre(log != nullptr) + cppverify::modifies(*log) + cppverify::post(v == 1 && *log == 1) + { + v = 1; + *log = 1; + } + + int v; +}; +// CHECK-DAG: Verified: Logged::Logged [backend=z3] + +int logged() + cppverify::post(cppverify::result == 2) +{ + int log = 0; + Logged l(&log); + return log + l.v; +} +// CHECK-DAG: Verified: logged [backend=z3] + +// Not supported, each with its function's located error. +struct Reads { + Reads() + cppverify::pre(v == 0) + : v(0) {} + + int v; +}; +// CHECK-DAG: error: Reads::Reads: a constructor's precondition cannot read its object, whose lifetime has not begun + +struct Delegates { + Delegates(int v) + cppverify::post(w == v) + : w(v) {} + Delegates() + cppverify::post(w == 0) + : Delegates(0) {} + + int w; +}; +// CHECK-DAG: error: Delegates::Delegates: delegating constructors are not verified yet + +struct Unverified { + Unverified() : v(0) {} + int v; +}; + +int uses_unverified() + cppverify::post(cppverify::result == 0) +{ + Unverified u; + return u.v; +} +// CHECK-DAG: error: uses_unverified: call to function without a verification contract: Unverified::Unverified diff --git a/clang/test/Verify/suite/loop_initialization.cpp b/clang/test/Verify/suite/loop_initialization.cpp new file mode 100644 index 0000000000..be551b7d30 --- /dev/null +++ b/clang/test/Verify/suite/loop_initialization.cpp @@ -0,0 +1,147 @@ +// RUN: not %cpp-verify --jobs=1 %s -- > %t 2>&1 +// RUN: FileCheck %s < %t +// RUN: FileCheck %s --check-prefix=SOUND < %t +// RUN: not %cpp-verify --jobs=1 --backend=bmc --unroll=5 %s -- 2>&1 \ +// RUN: | FileCheck %s --check-prefix=BMC +// +// An invariant holds at a loop's head together with its definedness: both +// are checked on entry and at the end of every iteration, so the reads it +// makes are initialized and in bounds there. A loop starts no lifetime, so +// it only initializes storage: what was initialized before it still is. +// +// No proof here holds only because no execution reaches its end. +// SOUND-NOT: vacuous + +int filled() + cppverify::post(cppverify::result == 0) +{ + int a[4]; + for (int i = 0; i < 4; i = i + 1) + cppverify::invariant(0 <= i && i <= 4) + cppverify::invariant(cppverify::forall(k, 0, i, a[k] == 0)) + cppverify::decreases(4 - i) + { + a[i] = 0; + } + return a[3]; +} +// CHECK-DAG: Verified: filled [backend=z3] +// BMC-DAG: Verified: filled [backend=bmc, bound=4] + +// The loop reads what was initialized before it, which no invariant states. +void incremented() +{ + int a[4]; + for (int j = 0; j < 4; j = j + 1) + cppverify::invariant(0 <= j && j <= 4) + cppverify::invariant(cppverify::forall(k, 0, j, a[k] == 1)) + cppverify::decreases(4 - j) + { + a[j] = 1; + } + for (int i = 0; i < 4; i = i + 1) + cppverify::invariant(0 <= i && i <= 4) + cppverify::decreases(4 - i) + { + a[i] = a[i] / 2; + } +} +// CHECK-DAG: Verified: incremented [backend=z3] + +// Storage the loop does not write stays initialized. +int kept() +{ + int x = 5; + int &r = x; + int a[2]; + for (int i = 0; i < 2; i = i + 1) + cppverify::invariant(0 <= i && i <= 2) + cppverify::decreases(2 - i) + { + a[i] = i; + } + return r; +} +// CHECK-DAG: Verified: kept [backend=z3] + +// An element the loop never writes is not initialized after it. +int partially_filled() +{ + int a[4]; + for (int i = 0; i < 3; i = i + 1) + cppverify::invariant(0 <= i && i <= 3) + cppverify::invariant(cppverify::forall(k, 0, i, a[k] == 0)) + cppverify::decreases(3 - i) + { + a[i] = 0; + } + return a[3]; +} +// CHECK-DAG: error: verification failed: partially_filled [{{.*}}::initialization@[[@LINE-2]]:3] + +// Nor is one it reads before writing. +int read_first() +{ + int a[4]; + int s = 0; + for (int i = 0; i < 4; i = i + 1) + cppverify::invariant(0 <= i && i <= 4) + cppverify::decreases(4 - i) + { + s = a[i]; + a[i] = s; + } + return 0; +} +// CHECK-DAG: error: verification failed: read_first [{{.*}}::initialization@[[@LINE-5]]:7] + +// Reading p[i] in an invariant bounds i at the head. +int last(const int *p, int n) + cppverify::pre(cppverify::valid(p, n) && n > 0) + cppverify::post(cppverify::result == p[n - 1]) +{ + int i = 0; + while (i + 1 < n) + cppverify::invariant(p[i] + 0 == p[i]) + cppverify::decreases(n - i) + { + i = i + 1; + } + return p[i]; +} +// CHECK-DAG: Verified: last [backend=z3] + +// So does a shift: its amount is in range at the head. +int log2_floor(int n) + cppverify::pre(n >= 1) + cppverify::post(0 <= cppverify::result && cppverify::result <= 31) +{ + int k = 0; + while (k < 30 && (1 << (k + 1)) <= n) + cppverify::invariant((1 << k) <= n) + cppverify::decreases(30 - k) + { + k = k + 1; + } + return k; +} +// CHECK-DAG: Verified: log2_floor [backend=z3] + +// The definedness is still checked where the invariant is. +void overrun() +{ + int c[4]; + c[0] = 0; + c[1] = 0; + c[2] = 0; + c[3] = 0; + int i = 0; + while (i < 4) + cppverify::invariant(0 <= i && i <= 4) + cppverify::invariant(c[i] == 0) + cppverify::decreases(4 - i) + { + i = i + 1; + } +} +// CHECK-DAG: error: verification failed: overrun [{{.*}}::dereference@[[@LINE-6]]:31#2] diff --git a/clang/test/Verify/suite/loop_local_frames.cpp b/clang/test/Verify/suite/loop_local_frames.cpp new file mode 100644 index 0000000000..9e8c660749 --- /dev/null +++ b/clang/test/Verify/suite/loop_local_frames.cpp @@ -0,0 +1,205 @@ +// RUN: not %cpp-verify --jobs=1 %s -- > %t 2>&1 +// RUN: FileCheck %s < %t +// RUN: FileCheck %s --check-prefix=SOUND < %t +// RUN: not %cpp-verify --jobs=1 --backend=bmc --unroll=5 %s -- 2>&1 \ +// RUN: | FileCheck %s --check-prefix=BMC +// +// A loop that writes local or dynamic storage through the pointer its +// allocation defined writes only that object: every other object keeps its +// value across the loop without an invariant saying so. +// +// No proof here holds only because no execution reaches its end. +// SOUND-NOT: vacuous + +int kept_value() + cppverify::post(cppverify::result == 5) +{ + int x = 5; + int &r = x; + int a[2]; + for (int i = 0; i < 2; i = i + 1) + cppverify::invariant(0 <= i && i <= 2) + cppverify::decreases(2 - i) + { + a[i] = i; + } + return r; +} +// CHECK-DAG: Verified: kept_value [backend=z3] +// BMC-DAG: Verified: kept_value [backend=bmc, bound=2] + +int other_array() + cppverify::post(cppverify::result == 7) +{ + int a[3]; + int b[2]; + b[0] = 3; + b[1] = 4; + for (int i = 0; i < 3; i = i + 1) + cppverify::invariant(0 <= i && i <= 3) + cppverify::decreases(3 - i) + { + a[i] = 0; + } + return b[0] + b[1]; +} +// CHECK-DAG: Verified: other_array [backend=z3] + +struct Pair { + int a; + int b; +}; + +// The loop reads one local record, kept in memory for its reference, and +// writes another object. +int record_read() + cppverify::post(cppverify::result == 2) +{ + Pair p; + p.a = 1; + p.b = 2; + int &pb = p.b; + int a[3]; + for (int i = 0; i < 3; i = i + 1) + cppverify::invariant(0 <= i && i <= 3) + cppverify::decreases(3 - i) + { + a[i] = p.a; + } + return pb; +} +// CHECK-DAG: Verified: record_read [backend=z3] + +// A loop that writes a parameter's object and a local one keeps a third. +int with_parameter(int *q) + cppverify::pre(q != nullptr) + cppverify::modifies(*q) + cppverify::post(cppverify::result == 9) +{ + int keep[1]; + keep[0] = 9; + int a[2]; + for (int i = 0; i < 2; i = i + 1) + cppverify::invariant(0 <= i && i <= 2) + cppverify::decreases(2 - i) + { + a[i] = i; + *q = i; + } + return keep[0]; +} +// CHECK-DAG: Verified: with_parameter [backend=z3] + +void set(int &r, int v) + cppverify::modifies(r) + cppverify::post(r == v) +{ + r = v; +} + +// A call in the loop writes an element of the local it is given. +int through_call() + cppverify::post(cppverify::result == 4) +{ + int x = 4; + int &r = x; + int a[2]; + a[0] = 1; + a[1] = 1; + for (int i = 0; i < 2; i = i + 1) + cppverify::invariant(0 <= i && i <= 2) + cppverify::decreases(2 - i) + { + set(a[i], 0); + } + return r; +} +// CHECK-DAG: Verified: through_call [backend=z3] + +// A dynamic object the loop does not write keeps its value too. +int dynamic_kept() + cppverify::post(cppverify::result == 6) +{ + int *p = new int(6); + int a[2]; + for (int i = 0; i < 2; i = i + 1) + cppverify::invariant(0 <= i && i <= 2) + cppverify::decreases(2 - i) + { + a[i] = i; + } + int v = *p; + delete p; + return v; +} +// CHECK-DAG: Verified: dynamic_kept [backend=z3] + +// A store through a reference to a local writes the one cell it binds. +int reference_written() + cppverify::post(cppverify::result == 3) +{ + int x = 0; + int &r = x; + int y = 3; + int &s = y; + for (int i = 0; i < 2; i = i + 1) + cppverify::invariant(0 <= i && i <= 2) + cppverify::decreases(2 - i) + { + r = i; + } + return s; +} +// CHECK-DAG: Verified: reference_written [backend=z3] + +// So does a call given that reference. +int reference_call() + cppverify::post(cppverify::result == 3) +{ + int x = 0; + int &r = x; + int y = 3; + int &s = y; + for (int i = 0; i < 2; i = i + 1) + cppverify::invariant(0 <= i && i <= 2) + cppverify::decreases(2 - i) + { + set(r, i); + } + return s; +} +// CHECK-DAG: Verified: reference_call [backend=z3] + +// What the loop writes is not kept. +int overwritten() + cppverify::post(cppverify::result == 7) +{ + int a[4]; + a[3] = 7; + for (int i = 0; i < 4; i = i + 1) + cppverify::invariant(0 <= i && i <= 4) + cppverify::decreases(4 - i) + { + a[i] = 0; + } + return a[3]; +} +// CHECK-DAG: error: verification failed: overwritten [{{.*}}::postcondition@ + +// Nor is a local written through a reference to it. +int through_reference() + cppverify::post(cppverify::result == 5) +{ + int x = 5; + int &r = x; + int a[2]; + for (int i = 0; i < 2; i = i + 1) + cppverify::invariant(0 <= i && i <= 2) + cppverify::decreases(2 - i) + { + a[i] = 0; + r = i; + } + return x; +} +// CHECK-DAG: error: verification failed: through_reference [{{.*}}::postcondition@ diff --git a/clang/test/Verify/suite/member_functions.cpp b/clang/test/Verify/suite/member_functions.cpp index eed3582248..c9ae66f99c 100644 --- a/clang/test/Verify/suite/member_functions.cpp +++ b/clang/test/Verify/suite/member_functions.cpp @@ -234,8 +234,8 @@ void self_copy_aliased(Counter &c) // CHECK-DAG: Verified: self_copy_aliased [backend=z3] // Not yet, each with its function's located error: virtual functions, -// members of classes with bases, constructors, destructors, and conversion -// functions. +// members of classes with bases, destructors (and the constructors of a +// class with one), and conversion functions. struct Shape { virtual int area() const cppverify::post(cppverify::result >= 0) @@ -272,6 +272,6 @@ struct Made { return v; } }; -// CHECK-DAG: error: Made::Made: constructors are not verified yet +// CHECK-DAG: error: Made::Made: constructors of a class that is not trivially copyable, whose copies or destruction run code, are not supported yet // CHECK-DAG: error: Made::~Made: destructors are not verified yet // CHECK-DAG: error: Made::operator int: conversion functions are unsupported diff --git a/clang/test/Verify/suite/record_references.cpp b/clang/test/Verify/suite/record_references.cpp index 793013fc11..b5b76351cf 100644 --- a/clang/test/Verify/suite/record_references.cpp +++ b/clang/test/Verify/suite/record_references.cpp @@ -385,6 +385,8 @@ int local_decay() } // CHECK-DAG: error: local_decay: array-to-pointer decay of automatic storage is unsupported until lexical lifetime and escape effects are modeled +// A record through a reference passed by value is its fields, read where +// they are. int by_copy(Counter c) cppverify::post(cppverify::result == c.n) { @@ -396,7 +398,7 @@ int whole_read(const Pair &p) { return by_copy(p.left); } -// CHECK-DAG: error: whole_read: a record or array read as a whole through a pointer or reference is unsupported; read its fields +// CHECK-DAG: Verified: whole_read [backend=z3] cppverify::proof void proof_reference(Counter &c) cppverify::post(true) diff --git a/clang/test/Verify/suite/record_values_in_memory.cpp b/clang/test/Verify/suite/record_values_in_memory.cpp new file mode 100644 index 0000000000..4012f3bb40 --- /dev/null +++ b/clang/test/Verify/suite/record_values_in_memory.cpp @@ -0,0 +1,152 @@ +// RUN: not %cpp-verify --jobs=1 %s -- > %t 2>&1 +// RUN: FileCheck %s < %t +// RUN: FileCheck %s --check-prefix=SOUND < %t +// RUN: not %cpp-verify --jobs=1 --backend=bmc %s -- 2>&1 \ +// RUN: | FileCheck %s --check-prefix=BMC +// +// A record kept in memory, a local object or one a pointer or reference +// addresses, is passed and returned by value as its fields, each read where +// it is, with the checks of that read: in bounds, valid, and initialized. +// +// No proof here holds only because no execution reaches its end. +// SOUND-NOT: vacuous + +struct Counter { + Counter(int l) + cppverify::post(n == 0 && limit == l) + : n(0), limit(l) {} + + int n; + int limit; +}; + +int limit_of(Counter c) + cppverify::post(cppverify::result == c.limit) +{ + return c.limit; +} + +// A constructed object, which is kept in memory, passed by value. +int passed() + cppverify::post(cppverify::result == 6) +{ + Counter c(6); + return limit_of(c); +} +// CHECK-DAG: Verified: passed [backend=z3] +// BMC-DAG: Verified: passed [backend=bmc, bound=0] + +// And returned by value. +Counter make(int l) + cppverify::post(cppverify::result.n == 0 && cppverify::result.limit == l) +{ + Counter c(l); + return c; +} +// CHECK-DAG: Verified: make [backend=z3] + +int made() + cppverify::post(cppverify::result == 9) +{ + Counter m = make(9); + return m.limit + m.n; +} +// CHECK-DAG: Verified: made [backend=z3] + +// A record through a pointer or a reference, by value. +int through_pointer(const Counter *p) + cppverify::pre(p != nullptr) + cppverify::post(cppverify::result == p->limit) +{ + return limit_of(*p); +} +// CHECK-DAG: Verified: through_pointer [backend=z3] + +int copied_through(const Counter *p) + cppverify::pre(p != nullptr) + cppverify::post(cppverify::result == p->n) +{ + Counter copy = *p; + return copy.n; +} +// CHECK-DAG: Verified: copied_through [backend=z3] + +int through_reference(const Counter &c) + cppverify::post(cppverify::result == c.limit) +{ + return limit_of(c); +} +// CHECK-DAG: Verified: through_reference [backend=z3] + +Counter returned_through(const Counter &c) + cppverify::post(cppverify::result.limit == c.limit) +{ + return c; +} +// CHECK-DAG: Verified: returned_through [backend=z3] + +// A whole record through a pointer, returned, and given to a spec. +Counter returned_pointee(const Counter *p) + cppverify::pre(p != nullptr) + cppverify::post(cppverify::result.n == p->n) +{ + return *p; +} +// CHECK-DAG: Verified: returned_pointee [backend=z3] + +cppverify::spec int spare(Counter c) { return c.limit - c.n; } + +int spare_of(const Counter *p) + cppverify::pre(p != nullptr && 0 <= p->n && p->n <= p->limit) + cppverify::post(cppverify::result == spare(*p)) +{ + return p->limit - p->n; +} +// CHECK-DAG: Verified: spare_of [backend=z3] + +// An element of an array member, read where it is: its index is checked +// against the array, though `items[2]` would be `count` and `spare`, inside +// the object. +struct Bag { + Counter items[2]; + int count; + int spare; +}; + +int element(const Bag *b, int k) + cppverify::pre(b != nullptr && 0 <= k && k < 2) + cppverify::post(cppverify::result == b->items[k].limit) +{ + return limit_of(b->items[k]); +} +// CHECK-DAG: Verified: element [backend=z3] + +int past_element(const Bag *b, int k) + cppverify::pre(b != nullptr && 0 <= k && k <= 2) +{ + return limit_of(b->items[k]); +} +// CHECK-DAG: error: verification failed: past_element [{{.*}}::bounds@[[@LINE-2]] + +// A copy reads every field, so each must be initialized. +struct Pair { + int a; + int b; +}; + +int pair_sum(Pair p) + cppverify::pre(-1000 < p.a && p.a < 1000 && -1000 < p.b && p.b < 1000) + cppverify::post(cppverify::result == p.a + p.b) +{ + return p.a + p.b; +} + +int half_initialized() + cppverify::post(true) +{ + Pair p; + int &a = p.a; + a = 1; + return pair_sum(p); +} +// CHECK-DAG: error: verification failed: half_initialized [{{.*}}::initialization@[[@LINE-2]] diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 64fbc1259c..1a65652ce0 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -249,6 +249,59 @@ of `ParseFunctionContractClauses` after the declarator's scopes), before the late-parsed body; an out-of-line definition's clauses enter its class's scope and `this`, as its trailing requires-clause does. +**Constructors:** `unsupportedConstructor` admits a constructor of a +trivially copyable class without bases that does not delegate and whose +members are scalars, pointers, and aggregates of them whose classes provide +no constructor. `convertFunction` marks it `VFunction::IsConstructor`, gives +`this` the lifetime companion `__cppverify_constructed_lifetime` (every +`CXXThisExpr`), so its accesses are those of local storage, initialization +checked, and generates the precondition that each leaf of `*this` is valid +with that identity, one live allocation, instead of a reference's +initialized object; nothing is assumed about the object's initialization. +Its body starts with its member initializers (`appendMemberInitializers`, +over `inits()`, which Sema keeps in execution order). `run()` checks every +leaf initialized in the final state (`emitConstructedChecks`, anchored at +the member); a loop in the body is framed by `this`'s origin, its entry +object, as a parameter's is. A local whose +initializer runs a non-trivial constructor is promoted (address discovery, +through `constructionOf`'s wrappers), and `appendObjectInitialization` runs +the construction there (`appendConstruction`): a provided constructor is a +`VCallStmt` with the object's address first; an implicit or defaulted +default constructor is its member initializers in place, recursively. At a +call of a constructor, `emitRecordActualChecks` checks the object's +validity but not its initialization, and `emitCallStmt` sets every leaf's +initialization bit after the frame. Records count as +supported types and layouts when trivially copyable rather than trivial, +since constructors no longer stop them. + +**Class invariants:** `entryClassInvariants` (a public, non-constructor +member function's) and `exitClassInvariants` (a public member function's and +every constructor's) give the class's `TypeContractInfo` invariants, which +`convertFunction` converts in its context (`this->f` loads) and adds as +generated pre- and postconditions of kind `type-invariant`; at exit +`DropExtentMarkers` makes each `valid(p, n)` the literal `true`. +`collectFieldExtents` scans the entry invariants with the written +preconditions, and `pointerFieldOfParameter` takes `this->f` (no parameter +declaration, named `this->f`), so an extent in an invariant is a synthetic +parameter of the member function, bound at its calls (3e). At a call, +`havocFootprints` frames a region footprint of a record parameter without an +extent as the cells of the record's leaves (`RecordCells`, from the callee's +layout at the actual's address), so the call stays a chain of stores; as one +byte range, a `HeapFrame`, a falsified claim after a constructor and a +member call took 60 s and ended `solver.timeout`, and fails in 0.3 s as cells. + +**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 +temporaries, as one `VLoadExpr` per field at its offset from the place's +address (`objectPlace`), each carrying the place's access condition, which +passivization asserts where the load is evaluated, and getting the load's +memory checks from UB instrumentation. A by-value argument +(`appendRecordCallArgument`), a record return (through a flattened +`__aggregate_return_N`, assigned before the lifetimes of the locals end), and +a copy into a flattened local (`appendRecordCopy`) use it; a record with a +member that is a record or an array is an error there. + **Pointers into objects:** `ASTConverter::subobjectPointer` lowers a decayed member array of a pointee and the address of a pointee's element, field, or nested record. In a statement (`SubobjectSink`) it asserts the place's access @@ -491,13 +544,14 @@ y_0 = x_3 + 1; ``` // while (cond) invariant(I) decreases(D) { body } -assert(I); // 1. invariant on entry +assert(defined(I)); assert(I); // 1. invariant on entry havoc(modified_vars + mem); // 2. forget loop-modified state + heap assume(frame(mem_entry, mem)); // cells outside the loop's write set kept -assume(I); // 3. inductive hypothesis +assume(init_entry => init); // initialization kept +assume(defined(I)); assume(I); // 3. inductive hypothesis if (cond) { // 4. if loop continues: [body in SSA] // execute one iteration - assert(I); // invariant preserved + assert(defined(I)); assert(I); // invariant preserved assert(D_new < D_old); // termination measure decreases assert(frame(mem_entry, mem)); // explicit loop modifies respected assume(false); // cut path @@ -515,9 +569,46 @@ origin is unknown the function's frame alone bounds the loop, since every store is checked against it. When every written region is a single cell the frame is a chain of stores of fresh values; otherwise it is a `HeapFrame(mem_entry, mem_head, regions)` relation. +Local and dynamic storage has no origin, so its writes are bounded by its +lifetime companion's pointer instead, when the loop assigns neither that +pointer nor its companion: a store whose address is such a pointer, a +reference to a local say, writes that one cell (`representedCell`); one +rooted at the pointer an allocation defined (`RepresentedObjects`: the +allocated type and size, recorded at `VAllocateStmt` and at a fresh-owned +call) writes that object (`representedRegions`), since its fields lie in the +layout and its fixed-array indices are checked. The object is its scalar +leaves from `VFunction::Layouts`, each a cell, so the frame stays a chain of +stores; with a byte range instead, Z3 found no counterexample to a claim the +loop falsifies within the timeout, and the leaves bound the same bytes. Without +a layout the object is its bytes. The function's own frame is never used +here, since a store to its own storage is not checked against it. Before +0.2 any store to local or dynamic storage left the loop unframed, so it +forgot every object. An explicit loop `cppverify::modifies` is also asserted at the end of each iteration and at each `continue` (obligation kind `frame`, located at the footprint). +**Definedness and initialization at the head.** Entry, the end of an +iteration, and each `continue` assert an invariant's definedness before the +invariant (`emitExprSafety`: its core checks and the memory checks +`instrumentUBChecks` recorded in `VWhileStmt::InvariantChecks`), so the head +assumes both (`assumeInvariantSafety`, over the same `exprSafetyChecks`): +what an invariant reads is in bounds and initialized there. Initialization +cannot be stated in a contract, so this is how a loop that fills local +storage knows what it has written. A store through local or dynamic storage +sets its cell's initialization bit, so it modifies the initialization heap +(`collectModified`), whose head version only grows: no lifetime begins or +ends in a loop (the converter rejects addressable declarations, allocation, +and deallocation there, and `startsLifetime` withholds the fact from a loop +that starts one), so the head assumes `forall a. init_entry[a] -> +init_head[a]`, triggered by reads of the head version +(`initializationKept`). Nothing frames the rest, since no claim needs a cell +to be uninitialized. Before 0.2 the head kept the initialization heap from +before the loop, and every iteration after the first saw the storage the +earlier ones wrote as uninitialized. Dafny checks an invariant's +well-formedness once, in the head's arbitrary state, from the invariants +before it, which suffices where storage is always initialized; here it is +proved where the invariant is. + **Termination.** An executable loop without `cppverify::decreases` contributes no measure obligation, and the driver reports the function `Unresolved` with `decreases.missing` unless BMC proved the unwinding or the loop's condition is diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 922e306a5a..7d3975ea99 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -231,6 +231,13 @@ while (i < n) - `cppverify::invariant(expr)`: must hold on entry and be preserved by each iteration. A loop whose condition is the constant false keeps every value it would change: after `while (false) { ... }` the state is the one before it. +- An invariant holds at the head of every iteration with its definedness, + since both are checked on entry and at the end of each iteration: the + reads it makes are in bounds and initialized there. A loop that fills a + local array states what it has written, + `cppverify::forall(k, 0, i, a[k] == 0)`, and that is what shows `a[k]` + initialized for `k < i`. No lifetime begins or ends in a loop, so what was + initialized before it stays initialized. - `cppverify::decreases(expr [, expr...])`: termination measure. Single expression must be non-negative and strictly decreasing. Tuple form is lex-ordered: `cppverify::decreases(a, b)` means `(a, b)` strictly decreases lexicographically, and only the first component that changes must stay non-negative. - Verification is total correctness, as in Verus: every executable loop needs `cppverify::decreases`, unless its condition is the constant false, so that @@ -261,7 +268,9 @@ for (int i = 0; i < n; i = i + 1) Without `cppverify::modifies`, a loop writes only the objects its stores and calls reach, inferred from the body: every other object keeps its value without - an invariant saying so. + an invariant saying so. Local and dynamic objects count alike: a store + through a local array, a local record, or a `new` pointer writes that + object, and one through a reference to a local writes the cell it binds. `do` loops place the clauses between the trailing condition and its semicolon: @@ -1147,8 +1156,11 @@ void put(Ring *r, int v) rejects `r->buf[8]`, whose address is `r->head`, inside `*r`; in `p->grid[i][j]` it bounds `j` by the row, so `grid[0][4]` is rejected although it is `grid[1][0]` in memory. -- A whole record or array read through a pointer (`Ring copy = *r;`) is - rejected. +- A record with scalar fields read as a whole through a pointer or a + reference, or kept in memory as a local object, is its fields, each read + where it is with that read's checks (bounds of the place, validity, + initialization): it may be passed, returned, and copied by value. A whole + record holding an array or a record (`Ring copy = *r;`) is rejected. - A pointer into the object, a decayed member array (`r->buf`) or the address of an element, a field, or a nested record (`&r->buf[i]`, `&r->head`, `&r->inner`), addresses only that subobject: the array it comes @@ -1294,9 +1306,36 @@ void reset_left(Pair &p) static member function is a free function. - Not yet, each an error naming the function: virtual functions (dispatch needs behavioral subtyping), member functions of classes with bases, - constructors and destructors, conversion functions, explicit object - parameters, rvalue- and volatile-qualified member functions; members of - class templates keep the template rule. + destructors, conversion functions, explicit object parameters, rvalue- and + volatile-qualified member functions; members of class templates keep the + template rule. + +### 3g. Constructors + +- A constructor runs on storage its caller allocated, as a Dafny + constructor's first phase assigns the fields of an object that exists but + is not yet initialized. At entry `this` is one live allocation at every + leaf (a generated precondition, which the caller shows for its object), + nothing is assumed about the initialization of its object, so a member + reads as initialized only once the constructor has written it, and every + leaf must be initialized by the constructor's end (`initialization`, + located at the member). Its precondition cannot read the object, and `aliases` cannot + name `this`. Its frame is `*this` and its own footprints. +- Member initializers run first, in declaration order (C++'s order, whatever + the written one): the member's initializer, else its in-class initializer, + else the default construction of its type. An implicit or defaulted + default constructor is exactly those initializers, run in place where the + object is defined; a constructor the class provides is a call, which needs + a contract. +- A caller passes the object's address as `this`, need not have initialized + it, and holds every leaf initialized after the call, with the + postcondition describing the values. A local constructed this way is kept + in memory. +- The class must be trivially copyable (copies are member-wise, and nothing + runs at the end of its lifetime). Not yet: delegating constructors, + members whose class provides a constructor, reference and bit-field + members, arrays of such objects, and `new` of a record. A constructed + object is passed and returned by value as 3b's records in memory are. ### 4. `cppverify::modifies(...)` frame condition @@ -1443,6 +1482,15 @@ For by-value parameters this is purely an optimization — correctness is identi fields just before the return, so a function that constructs and returns a struct violating its invariant is rejected. Struct construction/mutation/return is modelled by the backend (field stores become `var.field` SSA assignments). +- On a class with member functions (3f, 3g), the invariant is a generated + precondition of every public member function and a generated + postcondition of every public member function and constructor, checked + at every call, internal calls included: no call observes the object while + a member function breaks it, which is sound without pack/unpack. Private + and protected member functions take neither, so they may work on a broken + object. An extent marker in it, `valid(data, len)`, is a field extent + (3e) of `this` on entry; at exit it is `true`, since a postcondition + cannot carry a marker, and the next call checks the extent at its caller. - By design, the invariant is **not** asserted after each individual field write. Asserting the whole invariant mid-construction would spuriously fail while a multi-field struct is being initialised one field at a time (the other fields diff --git a/website/source/language/functions-loops.rst b/website/source/language/functions-loops.rst index 81312437e9..1c585c9cd4 100644 --- a/website/source/language/functions-loops.rst +++ b/website/source/language/functions-loops.rst @@ -454,10 +454,108 @@ increment, so ``a[0 : i]`` then covers the cell just written; the function's ``cppverify::modifies(a[0 : k])`` is the range ``[0, k)``, and the cells from ``k`` on keep their values without an invariant saying so. +Local and dynamic objects follow the same rule. A store through a local +array, a local record, or a ``new`` pointer writes that object, a store or a +call through a reference to a local writes the cell it binds, and every +other object keeps its value: + +.. cppverify-example: fails overwritten + +.. code-block:: cpp + + int other_array() + cv::post(cv::result == 7) + { + int a[3]; + int b[2]; + b[0] = 3; + b[1] = 4; + for (int i = 0; i < 3; i = i + 1) + cv::invariant(0 <= i && i <= 3) + cv::decreases(3 - i) + { + a[i] = 0; + } + return b[0] + b[1]; + } + + int overwritten() + cv::post(cv::result == 7) + { + int a[4]; + a[3] = 7; + for (int i = 0; i < 4; i = i + 1) + cv::invariant(0 <= i && i <= 4) + cv::decreases(4 - i) + { + a[i] = 0; + } + return a[3]; + } + +.. code-block:: text + + Verified: other_array [backend=z3] + frames.cpp:18:23: error: verification failed: overwritten [...::postcondition@18:23] (counterexample: ...) [backend=z3] [reason=counterexample] + +``overwritten`` fails because the loop writes ``a[3]``, which no invariant +describes. Before 0.2 a loop that wrote local or dynamic storage forgot the +value of every object, so ``other_array`` failed its postcondition. + After a normal exit the verifier knows ``I && !c`` about what the loop may change; variables the loop does not assign and memory outside its write set keep their values. A ``break`` or ``return`` leaves in its own state instead. +An invariant holds together with its definedness: establishment and +preservation check that what it reads is in bounds and initialized, and that +its shifts and divisions are defined, so the head of every iteration knows +both. A loop that fills a local array states what it has written, and the +reads that state it are what show those elements initialized, which no +contract can say directly: + +.. cppverify-example: fails partially_filled + +.. code-block:: cpp + + int filled() + cv::post(cv::result == 0) + { + int a[4]; + for (int i = 0; i < 4; i = i + 1) + cv::invariant(0 <= i && i <= 4) + cv::invariant(cv::forall(k, 0, i, a[k] == 0)) + cv::decreases(4 - i) + { + a[i] = 0; + } + return a[3]; + } + + int partially_filled() + { + int a[4]; + for (int i = 0; i < 3; i = i + 1) + cv::invariant(0 <= i && i <= 3) + cv::invariant(cv::forall(k, 0, i, a[k] == 0)) + cv::decreases(3 - i) + { + a[i] = 0; + } + return a[3]; + } + +.. code-block:: text + + Verified: filled [backend=z3] + fill.cpp:26:3: error: verification failed: partially_filled [...::initialization@26:3] (counterexample: ...) [backend=z3] [reason=counterexample] + +No lifetime begins or ends inside a loop, so what was initialized before it +stays initialized in every iteration and after it; an element the loop may +write is initialized at its head only where an invariant reads it. Before +0.2 the head kept the initialization of the state before the loop: every +iteration after the first saw the elements the earlier ones wrote as +uninitialized, and ``filled`` failed its ``initialization`` check. + .. note:: Contracts are mathematical, but the loop body runs on machine integers. diff --git a/website/source/language/limitations.rst b/website/source/language/limitations.rst index c89d899ddb..62b31833b3 100644 --- a/website/source/language/limitations.rst +++ b/website/source/language/limitations.rst @@ -152,9 +152,10 @@ C++ feature boundaries standard-layout records with nested record, pointer, and fixed-array members as promoted local objects, and through pointers, where each scalar field and element is a heap cell. - - Non-trivial, inherited, polymorphic, union, and bit-field records, - nested/pointer/array-bearing records used by value, and a whole record - or array read through a pointer (``Ring copy = *r;``). + - Records that are not trivially copyable, inherited, polymorphic, + union, and bit-field records, nested/pointer/array-bearing records + used by value, and a whole record holding an array or a record read + through a pointer (``Ring copy = *r;``). * - Functions - Free functions, member functions of classes without bases or virtual functions (:doc:`structs`), overloads, namespaces, contracts, direct calls, and @@ -162,7 +163,8 @@ C++ feature boundaries reference parameters and through automatic objects, with mutual recursion among functions of one kind (spec, proof, or executable). - Virtual functions, member functions of classes with bases, - constructors, destructors, conversion functions, + destructors, delegating constructors and the other constructors + :doc:`structs` lists, conversion functions, templates (one without contracts stops nothing unless verified code calls it; the contracts of a function or class template compile, instantiate, and are ignored with a warning, and one with contract @@ -222,7 +224,8 @@ Objects, classes, and RAII Flat records are currently value aggregates, not a general C++ object model. CppVerify does not yet model: -- constructors, destructors, copy/move special members, or RAII cleanup; +- destructors, copy/move special members of their own, or RAII cleanup + (constructors are verified, :doc:`structs`); - ``this`` and member-function cv/ref qualifiers; - class invariants over aliased mutable objects; - base subobjects, vtables, or virtual dispatch; diff --git a/website/source/language/structs.rst b/website/source/language/structs.rst index c1f81cade4..e8bc76c3d8 100644 --- a/website/source/language/structs.rst +++ b/website/source/language/structs.rst @@ -69,8 +69,41 @@ hold, so ``grid[0][4]`` is rejected even though it has the address of the body, and in postconditions and assertions, where a division by zero is checked too. -Reading a whole record or array through a pointer (``Ring copy = *r;``) is -not supported yet; read its fields instead. +A record with scalar fields is read as a whole through a pointer or a +reference field by field, each read checked where it is: ``Pair copy = *p;``, +``sum(*p)``, and ``return *p;`` read ``p->first`` and ``p->second``. + +.. code-block:: cpp + + struct Pair { + int first; + int second; + }; + + int sum(Pair p) + cv::pre(-1000 < p.first && p.first < 1000) + cv::pre(-1000 < p.second && p.second < 1000) + cv::post(cv::result == p.first + p.second) + { + return p.first + p.second; + } + + int sum_at(const Pair *p) + cv::pre(p != nullptr) + cv::pre(-1000 < p->first && p->first < 1000) + cv::pre(-1000 < p->second && p->second < 1000) + cv::post(cv::result == p->first + p->second) + { + return sum(*p); + } + +.. code-block:: text + + Verified: sum [backend=z3] + Verified: sum_at [backend=z3] + +A record holding an array or another record (``Ring copy = *r;``) is not +read as a whole yet; read its fields instead. Pointers into a record ---------------------- @@ -534,11 +567,92 @@ which ``reset_count`` may not. ``copy_from`` writes ``this->n`` and reads object twice. Not yet supported, each an error naming the function: virtual functions, -member functions of a class with bases, constructors and destructors, -conversion functions, and member functions of a class template (whose -contracts are ignored with a warning). A member call inside an expression -(``return n + get();``) is unsupported as a free function's is; assign its -result first. +member functions of a class with bases, destructors, conversion functions, +and member functions of a class template (whose contracts are ignored with a +warning). A member call inside an expression (``return n + get();``) is +unsupported as a free function's is; assign its result first. + +Constructors +------------ + +A constructor runs on storage its caller allocated. When it is entered, +every member of its object is uninitialized; its member initializers run +first, in declaration order whatever order they are written in, a member it +does not name taking its in-class initializer; and by its end it must have +initialized every member. Its postcondition describes the new object. A +caller passes the object's address as ``this`` and holds an initialized +object after the call: + +.. cppverify-example: fails Ring::Ring + +.. code-block:: cpp + + struct Ring { + Ring() + cv::post(head == 0 && count == 0) + cv::post(cv::forall(k, 0, 8, buf[k] == 0)) + : head(0), count(0) + { + for (int i = 0; i < 8; i = i + 1) + cv::invariant(0 <= i && i <= 8) + cv::invariant(head == 0 && count == 0) + cv::invariant(cv::forall(k, 0, i, buf[k] == 0)) + cv::decreases(8 - i) + { + buf[i] = 0; + } + } + + Ring(int first) + cv::post(head == 0 && count == 1 && buf[0] == first) + : head(0), count(1) + { + buf[0] = first; + } + + int buf[8]; + int head; + int count; + }; + + int fresh() + cv::post(cv::result == 0) + { + Ring r; + return r.count + r.buf[7]; + } + +.. code-block:: text + + Verified: Ring::Ring [backend=z3] + ring.cpp:24:7: error: verification failed: Ring::Ring [...::initialization@24:7#2] (counterexample: ...) [backend=z3] [reason=counterexample] + Verified: fresh [backend=z3] + +The second constructor initializes ``buf[0]`` alone, and the failure is +located at the member it leaves uninitialized, at its second element. The +loop of the first states what it has written, which is also what shows the +array initialized (:doc:`functions-loops`). + +- An implicit or defaulted default constructor is its members' + initializers, run where the object is defined: ``struct Point { int x = 3; + int y = 4; };`` then ``Point p;`` gives ``p.x == 3``. A constructor the + class provides needs a contract, as any function a verified one calls. +- A constructor's precondition cannot read its object, whose lifetime has + not begun, and ``cppverify::aliases`` cannot name ``this``: the object is + new. Its frame is its object and the footprints it lists. +- A member function called on the object before every member is + initialized reads them as initialized, which C++ does not require, so the + call is ``construct.unsupported``, as an out-parameter's is. +- Copies of such an object are its members' copies: its class must be + trivially copyable. +- Not yet, each an error naming the function: delegating constructors, + constructors of a class that is not trivially copyable (a destructor or a + copy operation of its own), of a class with members whose class provides a + constructor, with reference or bit-field members, or larger than 256 + bytes; arrays of objects with constructors; ``new`` of a record. +- A constructed object is kept in memory, and is passed, returned, and + copied by value as its fields, each read where it is (see `Records + through pointers`_). ``cppverify::type_invariant`` ----------------------------- @@ -581,6 +695,80 @@ The invariant may be temporarily broken **inside** the function while you assign time — it is only required to hold at the return (the encapsulation boundary), not after each individual field write. +Class invariants +~~~~~~~~~~~~~~~~ + +On a class with member functions, the invariant holds at the boundary of +every public member function, which assumes it on entry and must restore it, +and every constructor must establish it. It is checked at every call, +internal calls included, so no call observes the object while it is broken: + +.. cppverify-example: fails Meter::overflow + +.. code-block:: cpp + + class Meter { + public: + Meter() + cv::post(level == 0) + : level(0) {} + + void add(int d) + cv::pre(0 <= d && level + d <= 100) + cv::post(level == cv::old(level) + d) + { + level = level + d; + } + + void overflow() + cv::post(true) + { + level = 101; + } + + int get() const + cv::post(cv::result == level) + { + return level; + } + + int level; + + cv::type_invariant(0 <= level && level <= 100); + }; + + int filled() + cv::post(0 <= cv::result && cv::result <= 100) + { + Meter m; + m.add(30); + int v = m.get(); + return v; + } + +.. code-block:: text + + Verified: Meter::Meter [backend=z3] + Verified: Meter::add [backend=z3] + meter.cpp:28:33: error: verification failed: Meter::overflow [...::type-invariant@28:33] (counterexample: ...) [backend=z3] [reason=counterexample] + Verified: Meter::get [backend=z3] + Verified: filled [backend=z3] + +``filled`` knows ``0 <= v <= 100`` from the invariant ``get`` returns with. + +- A private or protected member function neither assumes nor restores it, + so it may work on the object while the invariant is broken; a public one + it calls then fails, at that call. +- A caller that writes a public field holds the invariant only if it keeps + it: the next public call checks it there. +- A function that takes the object by reference or pointer assumes nothing + of its invariant; to call a public member function on it, it states the + invariant in its own precondition. +- An extent of a pointer field, ``cv::valid(data, len)``, is assumed on + entry as in a precondition (`Extents of pointer fields`_). At exit it + states nothing; the next call checks it from what its caller knows, so a + member function that changes ``len`` states how. + View functions -------------- @@ -594,8 +782,11 @@ the view rather than the layout: cv::spec int total(Pair p) { return p.first + p.second; } The current aggregate model is intentionally narrow. A record passed or -returned by value must be trivial, standard-layout, and flat, with scalar -fields. A local object whose address is needed (it holds a fixed array, or a +returned by value must be trivially copyable, standard-layout, and flat, with +scalar fields; when the value is kept in memory (a local object, or a record +a pointer or reference addresses), each field is read where it is, with the +checks of that read, so a copy of a record with a field never written fails +its ``initialization`` check. A local object whose address is needed (it holds a fixed array, or a reference binds to one of its members) is promoted to an automatic object and may also have nested record, pointer, and fixed-array members. A record reached through a pointer or a reference may have the same members, and its diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index a59272ee8e..a6f7a162da 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -135,6 +135,27 @@ correct. after it could fail for values it never produces. Its state now carries over (:doc:`language/functions-loops`). +**Loops that initialize local storage.** Every iteration of a loop after the +first saw the local storage the earlier ones wrote as uninitialized, so a +loop filling a local array failed its ``initialization`` check, at the +invariant that stated what it had written or at a read after the loop. What +was initialized before a loop now stays initialized, and an invariant holds +at the head of each iteration with its definedness, which shows the elements +it reads initialized and in bounds (:doc:`language/functions-loops`). + +**Loops that write local storage.** A loop that wrote a local array, a local +record, a ``new`` object, or a local through a reference forgot the value of +every object, so a claim about a local the loop never touches failed after +it. Such a loop now writes only the objects it stores to, as a loop over +parameters always did (:doc:`language/functions-loops`). + +**Calls that write a record.** A call whose footprint is a record +parameter's object, as a member function's default ``modifies(*this)`` is, +framed its bytes with a quantified relation, and a claim the call +falsifies often ended ``solver.timeout`` instead of a counterexample. The +object is now its leaves, each one cell, and such a claim fails in a few +seconds (:doc:`language/structs`). + **Null minus null.** The difference of two null pointers failed its ``pointer-difference`` check; it is 0, as C++ defines (:doc:`language/pointers`). @@ -293,8 +314,32 @@ class without bases or virtual functions is verified now, as a function of ``this``: fields are cells of the object, ``c.bump()`` passes ``&c``, its clauses may name members declared after them (the complete-class context of C++26 contracts), and a non-const one without ``cppverify::modifies`` may -write its object. Virtual functions, constructors, destructors, and -conversion functions are errors naming the function (:doc:`language/structs`). +write its object. Virtual functions, destructors, and conversion functions +are errors naming the function (:doc:`language/structs`). + +**Constructors.** A constructor was an error (``constructors are not +verified yet``), and a class with one was not a supported type, so a local +of it could not be declared. A constructor of a trivially copyable class +without bases is verified now: its object is the caller's storage, every +member uninitialized at entry, its member initializers run in declaration +order with in-class initializers for the members it does not name, and it +must initialize every member by its end. ``Counter c(5);`` passes ``&c`` and +leaves an initialized object; an implicit or defaulted default constructor +runs its members' initializers in place (:doc:`language/structs`). + +**Class invariants.** A ``cppverify::type_invariant`` held only for records +passed and returned by value; member functions and constructors ignored it. +On a class now, every public member function assumes it on entry and must +restore it, every constructor must establish it, and it is checked at every +call, internal ones included; an extent of a pointer field in it is assumed +on entry (:doc:`language/structs`). + +**Records in memory by value.** A record kept in memory, a local object or +one a pointer or reference addresses, could not be passed, returned, or +(through a pointer) copied by value (``aggregate value use of an automatic +object is unsupported``, ``unsupported aggregate field base expression``). +Such a value is now its fields, each read where it is, with the bounds, +validity, and initialization checks of that read (:doc:`language/structs`). **Extents of pointer fields.** ``cv::valid(s->data, s->len)`` was an error (``valid marker requires a bare complete-object pointer and an integer element