diff --git a/clang/lib/Verify/CMakeLists.txt b/clang/lib/Verify/CMakeLists.txt index ee25e789a6..58327a2de8 100644 --- a/clang/lib/Verify/CMakeLists.txt +++ b/clang/lib/Verify/CMakeLists.txt @@ -29,6 +29,7 @@ add_clang_library(clangVerify Transform/Inductive.cpp Transform/Origins.cpp Transform/Ownership.cpp + Transform/OutParameters.cpp Transform/LoopUnroll.cpp Transform/SpecInline.cpp Transform/SubobjectBounds.cpp diff --git a/clang/lib/Verify/Driver/DumpIR.cpp b/clang/lib/Verify/Driver/DumpIR.cpp index a7833a20f1..0ee62cf1ca 100644 --- a/clang/lib/Verify/Driver/DumpIR.cpp +++ b/clang/lib/Verify/Driver/DumpIR.cpp @@ -381,7 +381,8 @@ void verify::dumpVFunction(const VFunction &Fn, llvm::raw_ostream &OS) { if (Fn.IntMode == VIntMode::Math) ind(OS, 1) << "int math\n"; for (const auto &P : Fn.Params) - ind(OS, 1) << "param " << P.first << "\n"; + ind(OS, 1) << "param " << P.first + << (Fn.OutParameters.count(P.first) ? " out" : "") << "\n"; ind(OS, 1) << "pre\n"; for (const auto &Pre : Fn.Preconditions) dumpVExpr(Pre.get(), OS, 2); diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp index 06d43a9b10..ce2fd0a830 100644 --- a/clang/lib/Verify/Driver/Verifier.cpp +++ b/clang/lib/Verify/Driver/Verifier.cpp @@ -17,6 +17,7 @@ #include "../IR/VStmt.h" #include "../Transform/LoopUnroll.h" #include "../Transform/Origins.h" +#include "../Transform/OutParameters.h" #include "../Transform/Ownership.h" #include "../Transform/Passivize.h" #include "../Transform/SpecInline.h" @@ -3139,6 +3140,7 @@ class Verifier { return true; } inferFreshOwnedReturns(Functions); + inferOutParameters(Functions); FunctionMap FnMap; for (const auto &Fn : Functions) diff --git a/clang/lib/Verify/Frontend/ASTConverter.cpp b/clang/lib/Verify/Frontend/ASTConverter.cpp index 3f258428cb..a614bac92d 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.cpp +++ b/clang/lib/Verify/Frontend/ASTConverter.cpp @@ -686,8 +686,20 @@ static const FunctionDecl *ownObjectCallee(const Expr *E) { return Callee && returnsOwnObject(Callee) ? Callee : nullptr; } +/// A reference to a const scalar, which a spec function reads as the value it +/// refers to: that value's type, else the type itself. +static QualType constScalarReferent(QualType Ty) { + const QualType Referent = Ty.getNonReferenceType(); + return Ty->isLValueReferenceType() && Referent.isConstQualified() && + !Referent.isVolatileQualified() && + Referent->isIntegralOrEnumerationType() + ? Referent.getUnqualifiedType() + : Ty; +} + static std::optional -findUnsupportedType(const FunctionDecl *FD, bool AllowScalarReferences) { +findUnsupportedType(const FunctionDecl *FD, bool AllowScalarReferences, + bool ConstScalarReferencesAreValues = false) { // By-value records keep their flattened SSA representation, so only records // whose direct fields are scalars may cross a function boundary. auto UnsupportedValueType = [](QualType Ty) { @@ -696,10 +708,14 @@ findUnsupportedType(const FunctionDecl *FD, bool AllowScalarReferences) { return Ty->isRecordType() && !isFlatScalarRecordType(Ty) && !VType::collectionKind(Ty); }; - if (UnsupportedValueType(FD->getReturnType()) && !returnsOwnObject(FD)) + auto Viewed = [&](QualType Ty) { + return ConstScalarReferencesAreValues ? constScalarReferent(Ty) : Ty; + }; + if (UnsupportedValueType(Viewed(FD->getReturnType())) && + !returnsOwnObject(FD)) return FD->getReturnType().getAsString(); for (const ParmVarDecl *Param : FD->parameters()) { - QualType Ty = Param->getType(); + QualType Ty = Viewed(Param->getType()); if (Ty->isReferenceType()) { if (!AllowScalarReferences || !(isSupportedScalarLValueReference(Ty) || @@ -915,6 +931,28 @@ VIntMode ASTConverter::specCallIntMode(const FunctionDecl *FD) const { return VIntMode::Math; } +/// For std::min(a, b) and std::max(a, b) of two integers, enumerations, or +/// bools: whether it is max. Nothing for any other function, such as the +/// overloads with a comparison or an initializer list. +static std::optional stdMinOrMax(const FunctionDecl *Callee, + const ASTContext &Ctx) { + if (!Callee || !Callee->isInStdNamespace() || !Callee->getIdentifier() || + !Callee->getPrimaryTemplate() || Callee->getNumParams() != 2) + return std::nullopt; + const bool IsMax = Callee->getName() == "max"; + if (!IsMax && Callee->getName() != "min") + return std::nullopt; + const QualType Result = Callee->getReturnType(); + const QualType T = Result.getNonReferenceType(); + if (!Result->isLValueReferenceType() || !T.isConstQualified() || + T.isVolatileQualified() || !T->isIntegralOrEnumerationType()) + return std::nullopt; + for (const ParmVarDecl *P : Callee->parameters()) + if (!Ctx.hasSameType(P->getType(), Result)) + return std::nullopt; + return IsMax; +} + /// A function as the verifier's messages name it, a template specialization /// with its arguments (`maxv`). static std::string functionName(const FunctionDecl *FD, @@ -2215,11 +2253,6 @@ static bool mentionsThis(const Stmt *S) { [](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()) @@ -3419,7 +3452,7 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { // carries that allocation's identity. if (Constructor) { VVarExpr Object("this", VType::makePtr(), SourceLocation(), - ConstructedObjectLifetime); + VConstructedObjectLifetime); Readable = nullptr; forEachObjectLeaf(ThisObject, 0, [&](QualType, uint64_t Offset) { auto Leaf = std::make_unique( @@ -3434,6 +3467,17 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { Readable = std::move(Leaf); return true; }); + // So is its last byte, which a call lending the object checks: the + // caller's at the constructor, the constructor's at a member call. + const uint64_t Size = Ctx.getTypeSizeInChars(ThisObject).getQuantity(); + if (Readable && Size > 1) + Readable = std::make_unique( + VBinOp::And, std::move(Readable), + std::make_unique( + VUnaryOp::ValidPtr, + objectLeafAddress(&Object, Size - 1, SourceLocation()), + VType::makeBool(), SourceLocation()), + VType::makeBool(), SourceLocation()); if (!Readable) Readable = std::make_unique(1, VType::makeBool(), SourceLocation()); @@ -3671,7 +3715,7 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { std::to_string(MaxAutomaticObjectBytes) + " bytes are not supported yet"); VVarExpr This("this", Fn->Params.front().second, FD->getLocation(), - ConstructedObjectLifetime); + VConstructedObjectLifetime); appendMemberInitializers(Constructor, &This, 0, FD->getLocation(), Fn->Body); } @@ -3930,6 +3974,27 @@ bool ASTConverter::checkLoopTermination(const Stmt *Loop, bool HasMeasure) { return true; } +std::unique_ptr ASTConverter::convertMinOrMax(const CallExpr *CE, + bool IsMax) { + // The standard's meaning ([alg.min.max]), whatever the library: the first + // argument unless the other is less (max) or greater (min) than it, which + // reads each argument once and has no definedness condition of its own. + auto A = convertExpr(CE->getArg(0)); + auto B = convertExpr(CE->getArg(1)); + if (!A || !B) + return nullptr; + const SourceLocation Loc = CE->getExprLoc(); + const VType Ty = A->Ty; + auto Less = IsMax ? std::make_unique(VBinOp::Lt, cloneVExpr(A.get()), + cloneVExpr(B.get()), + VType::makeBool(), Loc) + : std::make_unique(VBinOp::Lt, cloneVExpr(B.get()), + cloneVExpr(A.get()), + VType::makeBool(), Loc); + return std::make_unique(std::move(Less), std::move(B), + std::move(A), Ty, Loc); +} + std::unique_ptr ASTConverter::convertConstexprSpec(const FunctionDecl *FD) { llvm::SaveAndRestore Owner(ErrorFunction, functionIdentity(FD)); @@ -3937,21 +4002,35 @@ ASTConverter::convertConstexprSpec(const FunctionDecl *FD) { llvm::SaveAndRestore InContract(ErrorInContract, true); const size_t ErrorsAtStart = Errors.size(); nameParameters(FD, FD); - if (exceedsNestingLimit(FD, functionContract(FD)) || - hasIndirectMemoryAccess(FD)) - return nullptr; if (!FD->isConstexpr() || !FD->hasBody()) return nullptr; - if (FD->getReturnType()->isRecordType()) { - error(functionName(FD) + - ": aggregate-returning constexpr specs are unsupported"); - return nullptr; - } - if (auto Unsupported = findUnsupportedType(FD, false)) { - error(functionName(FD) + - ": unsupported C++ type in verification: " + *Unsupported); - return nullptr; - } + // One the verifier cannot lift is kept as a declaration that uses an + // unsupported construct, so that its users' verdicts name it. + auto Unlifted = [&](std::optional Message) { + if (Message) + error(FD->getLocation(), functionName(FD) + ": " + *Message); + auto Fn = std::make_unique(); + Fn->Name = functionName(FD); + Fn->Identity = functionIdentity(FD); + Fn->DeclLoc = FD->getLocation(); + Fn->IsSpec = true; + Fn->IsConstexprSpec = true; + return Fn; + }; + if (exceedsNestingLimit(FD, functionContract(FD))) + return Unlifted(std::nullopt); + if (hasIndirectMemoryAccess(FD)) + return Unlifted("a constexpr function read as a spec cannot read memory " + "through a pointer or an array"); + if (FD->getReturnType()->isRecordType()) + return Unlifted("aggregate-returning constexpr specs are unsupported"); + // A spec is a function of values: a reference to a const scalar, which it + // only reads, stands for the value it refers to, as an argument and as the + // result (std::max's `const T &`). + if (auto Unsupported = + findUnsupportedType(FD, /*AllowScalarReferences=*/false, + /*ConstScalarReferencesAreValues=*/true)) + return Unlifted("unsupported C++ type in verification: " + *Unsupported); auto Fn = std::make_unique(); Fn->Name = functionName(FD); @@ -3960,9 +4039,11 @@ ASTConverter::convertConstexprSpec(const FunctionDecl *FD) { Fn->IsConstexprSpec = true; IntMode = VIntMode::Machine; Fn->IntMode = IntMode; - Fn->ReturnType = VType::fromQualType(FD->getReturnType(), IntMode, Ctx); + Fn->ReturnType = + VType::fromQualType(constScalarReferent(FD->getReturnType()), IntMode, Ctx); CurrentFn = Fn.get(); + ValueReferences.clear(); for (const ParmVarDecl *P : FD->parameters()) { if (const RecordDecl *RD = getRecordFromType(P->getType())) { if (const RecordDecl *Definition = RD->getDefinition()) @@ -3971,8 +4052,11 @@ ASTConverter::convertConstexprSpec(const FunctionDecl *FD) { P->getNameAsString() + "." + Field->getNameAsString(), VType::fromQualType(Field->getType(), IntMode, Ctx)); } else { - Fn->Params.emplace_back(P->getNameAsString(), - VType::fromQualType(P->getType(), IntMode, Ctx)); + Fn->Params.emplace_back( + P->getNameAsString(), + VType::fromQualType(constScalarReferent(P->getType()), IntMode, Ctx)); + if (P->getType()->isReferenceType()) + ValueReferences.insert(P); } recordSourceVariable(P); } @@ -3988,10 +4072,12 @@ ASTConverter::convertConstexprSpec(const FunctionDecl *FD) { } if (Fn->Body.empty() && Errors.size() == ErrorsAtStart) { CurrentFn = nullptr; + ValueReferences.clear(); return nullptr; } collectLayouts(FD, *Fn); CurrentFn = nullptr; + ValueReferences.clear(); return Fn; } @@ -5483,7 +5569,7 @@ std::unique_ptr ASTConverter::convertExprImpl(const Expr *E) { } return std::make_unique( "this", CurrentFn->Params.front().second, E->getExprLoc(), - CurrentFn->IsConstructor ? ConstructedObjectLifetime : ""); + CurrentFn->IsConstructor ? VConstructedObjectLifetime : ""); } if (const auto *Decay = dyn_cast(E); Decay && Decay->getCastKind() == CK_ArrayToPointerDecay) { @@ -5639,7 +5725,7 @@ std::unique_ptr ASTConverter::convertExprImpl(const Expr *E) { E->getExprLoc()); } requireInitialized(VD); - if (VD->getType()->isReferenceType()) { + if (VD->getType()->isReferenceType() && !ValueReferences.count(VD)) { auto Address = convertLValueAddress(E); if (!Address) { error(CurrentFn->Name + ": unsupported reference value expression"); @@ -6114,6 +6200,17 @@ std::unique_ptr ASTConverter::convertExprImpl(const Expr *E) { integerValueString(EV.Val.getInt()), Ty, E->getExprLoc()); } } + if (std::optional IsMax = stdMinOrMax(Callee, Ctx)) + return convertMinOrMax(CE, *IsMax); + // The standard library's functions are not lifted: each library + // writes them its own way, so a proof would depend on which one. + if (Callee->isInStdNamespace() && calleeIsSpec(Callee) && + !functionContract(Callee)) { + error(CurrentFn->Name + ": " + Callee->getQualifiedNameAsString() + + " is not modeled: of the standard library, the verifier knows " + "std::min and std::max of two integers"); + return nullptr; + } if (calleeIsSpec(Callee)) { const VIntMode CalleeMode = specCallIntMode(Callee); const FunctionContractInfo *CalleeContract = functionContract(Callee); diff --git a/clang/lib/Verify/Frontend/ASTConverter.h b/clang/lib/Verify/Frontend/ASTConverter.h index cdb8defd6f..b56211f6ef 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.h +++ b/clang/lib/Verify/Frontend/ASTConverter.h @@ -74,6 +74,9 @@ class ASTConverter { std::map> InstantiationPoints; std::map ParameterNames; + /// The parameters of a lifted spec that refer to const scalars, which + /// stand for the values they refer to. + std::set ValueReferences; /// For a parameter a pack expands to, its index in the pack, `...[1]`. std::map PackElements; /// Names each parameter of \p FD after the declaration \p ContractDecl @@ -185,6 +188,9 @@ class ASTConverter { /// The address of a supported mutable global, or null after an error. std::unique_ptr globalAddress(const VarDecl *VD, SourceLocation Loc); std::unique_ptr convertConstexprSpec(const FunctionDecl *FD); + /// std::max(a, b), or std::min(a, b), of two integers, as the standard + /// defines it. + std::unique_ptr convertMinOrMax(const CallExpr *CE, bool IsMax); void noteSpecUse(const FunctionDecl *FD); std::unique_ptr convertExpr(const Expr *E); std::unique_ptr convertExprImpl(const Expr *E); diff --git a/clang/lib/Verify/IR/VExpr.h b/clang/lib/Verify/IR/VExpr.h index e0ace8e494..4b4818cdc5 100644 --- a/clang/lib/Verify/IR/VExpr.h +++ b/clang/lib/Verify/IR/VExpr.h @@ -31,6 +31,11 @@ inline constexpr const char *VInitializationHeapName = "__heap_init"; inline constexpr const char *VAllocationSizeHeapName = "__heap_alloc_size"; /// Allocation identity -> required alignment in target bytes. inline constexpr const char *VAllocationAlignHeapName = "__heap_alloc_align"; +/// The lifetime companion of a constructor's object, whose lifetime begins +/// at `this` when the constructor is entered: every `this` of a constructor +/// carries it. +inline constexpr const char *VConstructedObjectLifetime = + "__cppverify_constructed_lifetime"; enum class VBinOp { Add, diff --git a/clang/lib/Verify/IR/VStmt.cpp b/clang/lib/Verify/IR/VStmt.cpp index 8ec2bd2f14..60a01650f2 100644 --- a/clang/lib/Verify/IR/VStmt.cpp +++ b/clang/lib/Verify/IR/VStmt.cpp @@ -203,6 +203,7 @@ VFunction verify::cloneVFunction(const VFunction &Fn) { for (const auto &[Name, Field] : Fn.FieldParams) Out.FieldParams.emplace_back(Name, cloneVExpr(Field.get())); Out.ConstAddressParams = Fn.ConstAddressParams; + Out.OutParameters = Fn.OutParameters; Out.BoundedPointers = Fn.BoundedPointers; Out.ReturnFields = Fn.ReturnFields; Out.ExplicitPreconditionCount = Fn.ExplicitPreconditionCount; diff --git a/clang/lib/Verify/IR/VStmt.h b/clang/lib/Verify/IR/VStmt.h index dcdd0badfa..4d43bed959 100644 --- a/clang/lib/Verify/IR/VStmt.h +++ b/clang/lib/Verify/IR/VStmt.h @@ -438,6 +438,11 @@ struct VFunction { /// Pointer and reference parameters to const objects: the function /// writes nothing through them. std::set ConstAddressParams; + /// Pointer and reference parameters whose storage the body never reads + /// before writing it (inferOutParameters): a caller may pass storage that + /// is not initialized, and the body's reads of it are checked against what + /// it has written. + std::set OutParameters; /// Pointer variables that may address a subobject (a member array, a /// field): each has companions `name.__lo` and `name.__hi`, the bytes it /// may address, which every access and step through it must stay in. diff --git a/clang/lib/Verify/Transform/LoopUnroll.cpp b/clang/lib/Verify/Transform/LoopUnroll.cpp index cdb9564651..16005d2ad8 100644 --- a/clang/lib/Verify/Transform/LoopUnroll.cpp +++ b/clang/lib/Verify/Transform/LoopUnroll.cpp @@ -261,6 +261,7 @@ VFunction LoopUnroller::unroll(const VFunction &Fn, unsigned K) { for (const auto &[Name, Field] : Fn.FieldParams) Out.FieldParams.emplace_back(Name, cloneVExpr(Field.get())); Out.ConstAddressParams = Fn.ConstAddressParams; + Out.OutParameters = Fn.OutParameters; Out.BoundedPointers = Fn.BoundedPointers; Out.ReturnFields = Fn.ReturnFields; Out.ExplicitPreconditionCount = Fn.ExplicitPreconditionCount; diff --git a/clang/lib/Verify/Transform/OutParameters.cpp b/clang/lib/Verify/Transform/OutParameters.cpp new file mode 100644 index 0000000000..f37b42ec67 --- /dev/null +++ b/clang/lib/Verify/Transform/OutParameters.cpp @@ -0,0 +1,736 @@ +//===--- OutParameters.cpp ------------------------------------------------===// +// +// A parameter's storage needs to be initialized at entry only where the +// function may read it before writing it, as C# requires of an `out` +// parameter by definite assignment. The analysis is a conservative, +// flow-sensitive walk of the converted body per pointer or reference +// parameter: the leaves written on every path so far, at constant offsets +// from the parameter, cover the reads after them; a read anywhere else, a +// read of the entry state in a contract, a callee that may read the storage, +// or any use of the pointer other than an access, a null test, or a validity +// check makes it an input. Postconditions, loop invariants, and checks +// describe what the body has written, and the verifier checks their reads +// against it, so they are not reads here; but of storage the function never +// writes they read the caller's values, which makes it an input. The +// classification decides the contract only; the body is verified against +// it, its reads of an out-parameter checked against the initialization it +// tracks. +// +// The leaves of its object a function writes on every path to a return are +// initialized when it returns, which a generated postcondition states and +// the function's exit checks prove; a call writes them in its caller's walk. +// +//===----------------------------------------------------------------------===// +#include "OutParameters.h" +#include "UBChecks.h" +#include "llvm/ADT/STLExtras.h" +#include +#include +#include +#include +#include +#include +#include +#include + +using namespace clang; +using namespace verify; + +namespace { + +/// Per function identity, per parameter. +template +using PerParameter = std::map>; +using FunctionsByIdentity = std::map; + +const VExpr *stripCasts(const VExpr *E) { + while (E && E->K == VExpr::Cast) + E = static_cast(E)->Inner.get(); + return E; +} + +bool isVar(const VExpr *E, const std::string &Name) { + E = stripCasts(E); + return E && E->K == VExpr::Var && + static_cast(E)->Name == Name; +} + +bool mentions(const VExpr *E, const std::string &Name) { + if (!E) + return false; + if (E->K == VExpr::Var) + return static_cast(E)->Name == Name; + bool Found = false; + forEachVExprChild( + E, [&](const VExpr *Child) { Found = Found || mentions(Child, Name); }); + return Found; +} + +std::optional constantValue(const VExpr *E) { + E = stripCasts(E); + if (!E) + return std::nullopt; + if (E->K == VExpr::Literal) { + const std::string &Text = static_cast(E)->Value; + char *End = nullptr; + errno = 0; + const long long Value = std::strtoll(Text.c_str(), &End, 10); + if (errno || Text.empty() || *End) + return std::nullopt; + return Value; + } + if (E->K != VExpr::BinOp) + return std::nullopt; + const auto *B = static_cast(E); + auto L = constantValue(B->Lhs.get()); + auto R = constantValue(B->Rhs.get()); + if (!L || !R || *L < 0 || *R < 0 || *L > (1 << 30) || *R > (1 << 30)) + return std::nullopt; + switch (B->Op) { + case VBinOp::Add: + return *L + *R; + case VBinOp::Mul: + return *L * *R; + default: + return std::nullopt; + } +} + +/// The byte offset of an address from Param when it is the parameter plus +/// constants. +std::optional offsetFrom(const VExpr *E, const std::string &Param) { + E = stripCasts(E); + if (isVar(E, Param)) + return 0; + if (!E || E->K != VExpr::BinOp) + return std::nullopt; + const auto *B = static_cast(E); + if (B->Op != VBinOp::Add || B->Lhs->Ty.Kind != VTypeKind::Ptr) + return std::nullopt; + auto Base = offsetFrom(B->Lhs.get(), Param); + auto Step = constantValue(B->Rhs.get()); + if (!Base || !Step || *Step < 0) + return std::nullopt; + return *Base + static_cast(*Step); +} + +/// The leaves of the object a parameter of Fn addresses, as offsets: those +/// of its record layout, or one scalar at offset 0. +std::optional> pointeeLeaves(const VFunction &Fn, + const std::string &Param) { + auto Record = Fn.RecordParams.find(Param); + if (Record == Fn.RecordParams.end()) + return std::set{0}; + auto Layout = std::find_if( + Fn.Layouts.begin(), Fn.Layouts.end(), + [&](const VObjectLayout &L) { return L.TypeIdentity == Record->second; }); + if (Layout == Fn.Layouts.end()) + return std::nullopt; + std::set Leaves; + for (const VObjectLeaf &Leaf : Layout->Leaves) { + std::vector Offsets = {Leaf.OffsetBytes}; + for (const VObjectRepeat &Repeat : Leaf.Repeats) { + std::vector Next; + for (uint64_t Base : Offsets) + for (uint64_t K = 0; K < Repeat.Count; ++K) { + if (Next.size() + Leaves.size() > 4096) + return std::nullopt; + Next.push_back(Base + K * Repeat.StrideBytes); + } + Offsets = std::move(Next); + } + Leaves.insert(Offsets.begin(), Offsets.end()); + } + return Leaves; +} + +/// The leaves written on every path to a point, by offset; an ended path +/// (after a return, break, or continue) reaches no later point. +struct Written { + std::set Leaves; + bool Ended = false; + + static Written join(const Written &A, const Written &B) { + if (A.Ended) + return B; + if (B.Ended) + return A; + Written Out; + std::set_intersection(A.Leaves.begin(), A.Leaves.end(), B.Leaves.begin(), + B.Leaves.end(), + std::inserter(Out.Leaves, Out.Leaves.begin())); + return Out; + } +}; + +class Analysis { + const VFunction &Fn; + const std::string &Param; + const FunctionsByIdentity &Functions; + /// The out-parameters assumed so far. + const PerParameter &Out; + /// The leaves each function writes on every path, found so far. + const PerParameter> &Writes; + /// Whether the walk ends at the first read: the leaves written are not + /// needed then. + bool StopAtRead; + bool Reads = false; + /// A store through the parameter, or a call passing it to a callee's + /// out-parameter. + bool WritesSomewhere = false; + /// A postcondition, invariant, or check reads its storage. + bool LaterStateReads = false; + /// The leaves written at every return. + std::optional Exit; + + void read(uint64_t Offset, const Written &W) { + if (!W.Leaves.count(Offset)) + Reads = true; + } + + bool stopped(const Written &W) const { + return W.Ended || (Reads && StopAtRead); + } + + void exit(const Written &W) { + if (W.Ended) + return; + Exit = Exit ? Written::join(*Exit, W) : W; + } + + /// Any access through the parameter, where E is evaluated. + bool readsStorage(const VExpr *E) const { + if (!E) + return false; + if (E->K == VExpr::Load && + mentions(static_cast(E)->Ptr.get(), Param)) + return true; + if (E->K == VExpr::SpecCall) { + const auto *C = static_cast(E); + auto Callee = Functions.find(C->CalleeIdentity); + const bool ReadsHeap = C->ReadsHeap || Callee == Functions.end() || + Callee->second->ReadsHeap; + if (ReadsHeap && llvm::any_of(C->Args, [&](const auto &Arg) { + return mentions(Arg.get(), Param); + })) + return true; + } + bool Found = false; + forEachVExprChild( + E, [&](const VExpr *Child) { Found = Found || readsStorage(Child); }); + return Found; + } + + /// The reads of a clause about a later state: those under `old` read the + /// entry state. + void laterStateReads(const VExpr *E) { + LaterStateReads = LaterStateReads || readsStorage(E); + oldReads(E); + } + + void oldReads(const VExpr *E) { + if (!E) + return; + if (E->K == VExpr::Old) { + Reads = + Reads || readsStorage(static_cast(E)->Inner.get()); + return; + } + forEachVExprChild(E, [&](const VExpr *Child) { oldReads(Child); }); + } + + /// An address computed from the parameter: its index expressions are + /// evaluated, and anything but a step from the parameter is a use of it. + void address(const VExpr *E, const Written &W) { + E = stripCasts(E); + if (isVar(E, Param)) + return; + if (E && E->K == VExpr::BinOp) { + const auto *B = static_cast(E); + if ((B->Op == VBinOp::Add || B->Op == VBinOp::Sub) && + B->Lhs->Ty.Kind == VTypeKind::Ptr && mentions(B->Lhs.get(), Param)) { + address(B->Lhs.get(), W); + expr(B->Rhs.get(), W); + return; + } + } + Reads = true; + } + + void expr(const VExpr *E, const Written &W) { + if (!E) + return; + switch (E->K) { + case VExpr::Var: + // The pointer itself escapes: copied, compared, returned, converted. + if (static_cast(E)->Name == Param) + Reads = true; + return; + case VExpr::Load: { + const auto *L = static_cast(E); + expr(L->AccessCondition.get(), W); + if (!mentions(L->Ptr.get(), Param)) { + expr(L->Ptr.get(), W); + return; + } + if (auto Offset = offsetFrom(L->Ptr.get(), Param)) + read(*Offset, W); + else + Reads = true; + return; + } + case VExpr::Cast: { + // A null test reads nothing. + const VExpr *Inner = static_cast(E)->Inner.get(); + if (E->Ty.Kind == VTypeKind::Bool && Inner->Ty.Kind == VTypeKind::Ptr && + mentions(Inner, Param)) { + address(Inner, W); + return; + } + break; + } + case VExpr::BinOp: { + const auto *B = static_cast(E); + if (B->Op == VBinOp::Eq || B->Op == VBinOp::Ne) + for (auto [Pointer, Other] : {std::pair(B->Lhs.get(), B->Rhs.get()), + std::pair(B->Rhs.get(), B->Lhs.get())}) + if (Pointer->Ty.Kind == VTypeKind::Ptr && mentions(Pointer, Param) && + constantValue(Other) == 0) { + address(Pointer, W); + return; + } + break; + } + case VExpr::UnaryOp: { + const auto *U = static_cast(E); + if (U->Op == VUnaryOp::ValidPtr && mentions(U->Operand.get(), Param)) { + address(U->Operand.get(), W); + return; + } + if (U->Op == VUnaryOp::InitializedPtr && + mentions(U->Operand.get(), Param)) { + Reads = true; + return; + } + break; + } + case VExpr::SpecCall: + if (readsStorage(E)) { + Reads = true; + return; + } + // A spec that does not read memory computes from the address alone. + for (const auto &Arg : static_cast(E)->Args) + if (mentions(Arg.get(), Param)) + address(Arg.get(), W); + else + expr(Arg.get(), W); + return; + case VExpr::Old: + Reads = + Reads || readsStorage(static_cast(E)->Inner.get()); + return; + default: + break; + } + forEachVExprChild(E, [&](const VExpr *Child) { expr(Child, W); }); + } + + void call(const VCallStmt &C, Written &W) { + auto CalleeIt = Functions.find(C.CalleeIdentity); + const VFunction *Callee = + CalleeIt == Functions.end() ? nullptr : CalleeIt->second; + std::set Initialized; + for (unsigned I = 0; I < C.Args.size(); ++I) { + const VExpr *Arg = C.Args[I].get(); + if (!mentions(Arg, Param)) { + expr(Arg, W); + continue; + } + if (Arg->Ty.Kind != VTypeKind::Ptr || !Callee || + I >= Callee->Params.size()) { + Reads = true; + continue; + } + const std::string &Formal = Callee->Params[I].first; + address(Arg, W); + auto Offset = offsetFrom(Arg, Param); + if (auto CalleeWrites = Writes.find(Callee->Identity); + Offset && CalleeWrites != Writes.end()) + if (auto Leaves = CalleeWrites->second.find(Formal); + Leaves != CalleeWrites->second.end()) + for (uint64_t Leaf : Leaves->second) + Initialized.insert(*Offset + Leaf); + auto CalleeOut = Out.find(Callee->Identity); + if (CalleeOut != Out.end() && CalleeOut->second.count(Formal)) { + WritesSomewhere = true; + continue; + } + // A callee that may read the storage it receives reads all of it, and + // one with an extent reads more than this analysis follows. + auto Leaves = pointeeLeaves(*Callee, Formal); + if (!Offset || !Leaves || + llvm::any_of(Callee->ValidExtents, [&](const VValidExtent &E) { + return E.Base == Formal; + })) { + Reads = true; + continue; + } + for (uint64_t Leaf : *Leaves) + read(*Offset + Leaf, W); + } + W.Leaves.insert(Initialized.begin(), Initialized.end()); + } + + void stmts(const std::vector> &Stmts, Written &W) { + for (const auto &S : Stmts) { + if (stopped(W)) + return; + stmt(*S, W); + } + } + + void stmt(const VStmt &S, Written &W) { + if (isBindingInitialization(S, Param)) + return; + switch (S.K) { + case VStmt::Assign: + expr(static_cast(S).Value.get(), W); + return; + case VStmt::Store: { + const auto &St = static_cast(S); + expr(St.Value.get(), W); + expr(St.AccessCondition.get(), W); + if (!mentions(St.Ptr.get(), Param)) { + expr(St.Ptr.get(), W); + return; + } + address(St.Ptr.get(), W); + WritesSomewhere = true; + if (auto Offset = offsetFrom(St.Ptr.get(), Param)) + W.Leaves.insert(*Offset); + return; + } + case VStmt::Allocate: + expr(static_cast(S).Initializer.get(), W); + return; + case VStmt::Free: + expr(static_cast(S).Ptr.get(), W); + return; + case VStmt::If: { + const auto &I = static_cast(S); + expr(I.Cond.get(), W); + Written Then = W, Else = W; + stmts(I.Then, Then); + stmts(I.Else, Else); + W = Written::join(Then, Else); + return; + } + case VStmt::While: { + const auto &L = static_cast(S); + // Every iteration starts with at least the leaves written before the + // loop, and the loop may run no iteration. + expr(L.Cond.get(), W); + for (const auto &Invariant : L.Invariants) + laterStateReads(Invariant.get()); + for (const auto &Measure : L.Decreases) + expr(Measure.get(), W); + for (const VFootprint &F : L.Modifies) + expr(F.Count.get(), W); + Written Body = W; + stmts(L.Body, Body); + return; + } + case VStmt::Call: + call(static_cast(S), W); + return; + case VStmt::Assert: + expr(static_cast(S).Cond.get(), W); + return; + case VStmt::Assume: + expr(static_cast(S).Cond.get(), W); + return; + case VStmt::Return: + expr(static_cast(S).Value.get(), W); + exit(W); + W.Ended = true; + return; + case VStmt::Break: + case VStmt::Continue: + W.Ended = true; + return; + case VStmt::Seq: + stmts(static_cast(S).Stmts, W); + return; + case VStmt::GhostBlock: { + Written Ghost = W; + stmts(static_cast(S).Body, Ghost); + return; + } + case VStmt::ContractAssert: + laterStateReads(static_cast(S).Cond.get()); + return; + case VStmt::Havoc: + if (static_cast(S).Target == Param) + Reads = true; + return; + case VStmt::EndLifetime: + case VStmt::RevealWithFuel: + case VStmt::HideSpec: + case VStmt::RevealSpec: + return; + } + } + +public: + Analysis(const VFunction &Fn, const std::string &Param, + const FunctionsByIdentity &Functions, const PerParameter &Out, + const PerParameter> &Writes, bool StopAtRead) + : Fn(Fn), Param(Param), Functions(Functions), Out(Out), Writes(Writes), + StopAtRead(StopAtRead) {} + + /// The converter's check that a reference bound to part of an object + /// reads as initialized: initialization of the object asserted, of the + /// part assumed. Binding reads nothing, and an out-parameter's parts are + /// tracked themselves, so neither applies to one. + static bool isBindingInitialization(const VStmt &S, + const std::string &Param) { + auto IsInitialized = [&](const VExpr *C) { + return C && C->K == VExpr::UnaryOp && + static_cast(C)->Op == + VUnaryOp::InitializedPtr && + mentions(C, Param); + }; + if (S.K == VStmt::Assert) { + const auto &A = static_cast(S); + return A.ProofKind == ProofObligationKind::Initialization && + IsInitialized(A.Cond.get()); + } + if (S.K == VStmt::Assume) { + const VExpr *C = static_cast(S).Cond.get(); + return C && C->K == VExpr::BinOp && + static_cast(C)->Op == VBinOp::And && + IsInitialized(static_cast(C)->Rhs.get()); + } + return false; + } + + void run() { + for (const auto &Pre : Fn.Preconditions) + Reads = Reads || readsStorage(Pre.get()); + for (const auto &E : Fn.Recommends) + Reads = Reads || readsStorage(E.get()); + for (const auto &E : Fn.Decreases) + Reads = Reads || readsStorage(E.get()); + for (const auto &[Name, Assumes] : Fn.Behaviors) + Reads = Reads || readsStorage(Assumes.get()); + for (const auto &[Name, Field] : Fn.FieldParams) + Reads = Reads || readsStorage(Field.get()); + for (const VFootprint &F : Fn.Modifies) + Reads = Reads || readsStorage(F.Count.get()); + for (const VValidExtent &Extent : Fn.ValidExtents) + Reads = Reads || readsStorage(Extent.Length.get()); + for (const auto &Post : Fn.Postconditions) + laterStateReads(Post.get()); + Written W; + stmts(Fn.Body, W); + exit(W); + if (LaterStateReads && !WritesSomewhere) + Reads = true; + } + + /// Whether the function may read the parameter's storage before writing + /// it. + bool readsBeforeWriting() const { return Reads; } + + /// The leaves of the parameter's object written at every return. + std::set writtenAtExit() const { + std::set Out; + auto Leaves = pointeeLeaves(Fn, Param); + if (!Exit || !Leaves) + return Out; + for (uint64_t Leaf : Exit->Leaves) + if (Leaves->count(Leaf)) + Out.insert(Leaf); + return Out; + } +}; + +std::set candidates(const VFunction &Fn) { + std::set Out; + if (Fn.IsSpec || Fn.IsProof || Fn.IsExternalContract || Fn.IsTrusted || + Fn.IsBuiltin || Fn.UnsupportedConstruct || Fn.TotalExpressions) + return Out; + const std::set Assigned = assignedNames(Fn.Body); + for (const auto &[Name, Ty] : Fn.Params) { + if (Ty.Kind != VTypeKind::Ptr || Ty.PointeeSizeBytes == 0 || + Assigned.count(Name) || (Fn.IsConstructor && Name == "this") || + llvm::any_of(Fn.FieldParams, [&, &Name = Name](const auto &F) { + return F.first == Name; + })) + continue; + Out.insert(Name); + } + return Out; +} + +/// E without the initialization of storage that IsOut names: a conjunct +/// dropped, or true in its place elsewhere. +std::unique_ptr +withoutInitialization(std::unique_ptr E, + const std::function &IsOut) { + if (!E) + return E; + if (E->K == VExpr::UnaryOp) { + auto *U = static_cast(E.get()); + if (U->Op == VUnaryOp::InitializedPtr && IsOut(U->Operand.get())) + return std::make_unique(1, VType::makeBool(), E->Loc); + return E; + } + if (E->K != VExpr::BinOp) + return E; + auto *B = static_cast(E.get()); + if (B->Op != VBinOp::And && B->Op != VBinOp::Or) + return E; + B->Lhs = withoutInitialization(std::move(B->Lhs), IsOut); + B->Rhs = withoutInitialization(std::move(B->Rhs), IsOut); + auto IsTrue = [](const VExpr *X) { + return X->K == VExpr::Literal && + static_cast(X)->Value == "1"; + }; + if (B->Op == VBinOp::And && IsTrue(B->Rhs.get())) + return std::move(B->Lhs); + if (B->Op == VBinOp::And && IsTrue(B->Lhs.get())) + return std::move(B->Rhs); + return E; +} + +void dropBindingInitialization(std::vector> &Stmts, + const std::set &OutParams) { + auto IsOut = [&](const VExpr *X) { + return llvm::any_of( + OutParams, [&](const std::string &Name) { return mentions(X, Name); }); + }; + std::vector> Kept; + for (auto &S : Stmts) { + const bool Binding = llvm::any_of(OutParams, [&](const std::string &Name) { + return Analysis::isBindingInitialization(*S, Name); + }); + if (Binding && S->K == VStmt::Assert) + continue; + if (Binding) { + auto &A = static_cast(*S); + A.Cond = withoutInitialization(std::move(A.Cond), IsOut); + } + switch (S->K) { + case VStmt::If: { + auto &I = static_cast(*S); + dropBindingInitialization(I.Then, OutParams); + dropBindingInitialization(I.Else, OutParams); + break; + } + case VStmt::While: + dropBindingInitialization(static_cast(*S).Body, OutParams); + break; + case VStmt::Seq: + dropBindingInitialization(static_cast(*S).Stmts, OutParams); + break; + case VStmt::GhostBlock: + dropBindingInitialization(static_cast(*S).Body, + OutParams); + break; + default: + break; + } + Kept.push_back(std::move(S)); + } + Stmts = std::move(Kept); +} + +} // namespace + +void verify::inferOutParameters( + std::vector> &Functions) { + FunctionsByIdentity ByIdentity; + PerParameter Out; + for (const auto &Fn : Functions) { + ByIdentity[Fn->Identity] = Fn.get(); + for (const std::string &Param : candidates(*Fn)) + Out[Fn->Identity][Param] = true; + } + // The leaves written on every path, a least fixpoint: a call writes what + // the callee was found to write, recursive calls included, so nothing is + // assumed of a call that only induction would show. + PerParameter> Writes; + for (bool Changed = true; Changed;) { + Changed = false; + for (const auto &Fn : Functions) + for (const auto &[Param, Unused] : Out[Fn->Identity]) { + Analysis A(*Fn, Param, ByIdentity, Out, Writes, /*StopAtRead=*/false); + A.run(); + std::set &Known = Writes[Fn->Identity][Param]; + std::set Found = A.writtenAtExit(); + if (Found != Known) { + Known = std::move(Found); + Changed = true; + } + } + } + // The out-parameters, a greatest fixpoint: a call that passes the storage + // on to a callee's out-parameter reads nothing, recursive calls included. + for (bool Changed = true; Changed;) { + Changed = false; + for (const auto &Fn : Functions) { + auto &Params = Out[Fn->Identity]; + for (auto It = Params.begin(); It != Params.end();) { + Analysis A(*Fn, It->first, ByIdentity, Out, Writes, + /*StopAtRead=*/true); + A.run(); + if (A.readsBeforeWriting()) { + It = Params.erase(It); + Changed = true; + } else { + ++It; + } + } + } + } + for (auto &Fn : Functions) { + for (const auto &[Param, Unused] : Out[Fn->Identity]) + Fn->OutParameters.insert(Param); + if (Fn->OutParameters.empty()) + continue; + auto IsOutParameter = [&](const VExpr *X) { + X = stripCasts(X); + return X && X->K == VExpr::Var && + Fn->OutParameters.count(static_cast(X)->Name); + }; + for (size_t I = 0; I != Fn->Preconditions.size(); ++I) + if (preconditionKind(*Fn, I) == ProofObligationKind::PointerValidity) + Fn->Preconditions[I] = withoutInitialization( + std::move(Fn->Preconditions[I]), IsOutParameter); + dropBindingInitialization(Fn->Body, Fn->OutParameters); + // What the body writes on every path is initialized at every return. + for (const std::string &Param : Fn->OutParameters) { + auto Source = Fn->SourceVariables.find(Param); + const SourceLocation Loc = Source != Fn->SourceVariables.end() + ? Source->second.Loc + : Fn->DeclLoc; + for (uint64_t Leaf : Writes[Fn->Identity][Param]) { + std::unique_ptr Address = + std::make_unique(Param, VType::makePtr(), Loc); + if (Leaf != 0) + Address = std::make_unique( + VBinOp::Add, std::move(Address), + std::make_unique(std::to_string(Leaf), + VType::makePtr(), Loc), + VType::makePtr(), Loc); + addPostcondition(*Fn, + std::make_unique( + VUnaryOp::InitializedPtr, std::move(Address), + VType::makeBool(), Loc), + ProofObligationKind::Initialization); + } + } + } +} diff --git a/clang/lib/Verify/Transform/OutParameters.h b/clang/lib/Verify/Transform/OutParameters.h new file mode 100644 index 0000000000..6a9cd220a2 --- /dev/null +++ b/clang/lib/Verify/Transform/OutParameters.h @@ -0,0 +1,26 @@ +//===--- OutParameters.h - Parameters written before read -------*- C++ -*-===// +// +// Finds the pointer and reference parameters whose storage a verified body +// never reads before writing it, so that a caller may pass storage that is +// not initialized ([dcl.init.ref], [basic.indet]): binding a reference or +// passing a pointer reads nothing. +// +//===----------------------------------------------------------------------===// +#ifndef LLVM_CLANG_VERIFY_TRANSFORM_OUTPARAMETERS_H +#define LLVM_CLANG_VERIFY_TRANSFORM_OUTPARAMETERS_H + +#include "../IR/VStmt.h" + +namespace clang { +namespace verify { + +/// Sets VFunction::OutParameters of every function with a verified body, and +/// removes from their generated validity preconditions the initialization +/// they no longer require, and from their bodies the initialization a +/// reference bound to part of one assumed of its object. +void inferOutParameters(std::vector> &Functions); + +} // namespace verify +} // namespace clang + +#endif diff --git a/clang/lib/Verify/Transform/Passivize.cpp b/clang/lib/Verify/Transform/Passivize.cpp index 04e9f786b3..e9e81c0fbf 100644 --- a/clang/lib/Verify/Transform/Passivize.cpp +++ b/clang/lib/Verify/Transform/Passivize.cpp @@ -1740,8 +1740,7 @@ static constexpr const char *UnknownOriginNote = "returned by a call, so the object it addresses is not known"; static constexpr const char *OutParameterNote = "binding a reference or pointer parameter to storage that is not " - "initialized, since the callee is verified as reading initialized " - "storage"; + "initialized, which the callee may read before writing it"; static constexpr const char *UninitializedResultNote = "returning a pointer to storage that is not initialized, since callers " "read a returned pointer's storage as initialized"; @@ -2023,14 +2022,20 @@ static std::unique_ptr exactPointerSafety(const VExpr *Ptr, return makeAnd(std::move(NonNull), std::move(Valid), Loc); } -static std::unique_ptr initializedSafety(const VExpr *Ptr, - SourceLocation Loc, - bool ObjectModel = false) { +static std::unique_ptr +initializedSafety(const VExpr *Ptr, SourceLocation Loc, + bool ObjectModel = false, + const std::set *OutParameters = nullptr) { const VExpr *Base = pointerBase(Ptr); if (!Base) return makeBoolLiteral(false, Loc); if (isGlobalCell(Base)) return makeBoolLiteral(true, Loc); + // An out-parameter's storage is initialized where the function wrote it. + if (OutParameters && Base->K == VExpr::Var && + OutParameters->count(static_cast(Base)->Name)) + return std::make_unique( + VUnaryOp::InitializedPtr, cloneVExpr(Ptr), VType::makeBool(), Loc); // Abstract storage is initialized. if (ObjectModel && !hasPointerProvenance(Ptr)) return makeBoolLiteral(true, Loc); @@ -2152,10 +2157,11 @@ collectSafety(const VExpr *E, const FunctionMap *FnMap, const std::vector *ValidExtents, const std::set *PointerParams, SafetyChecks &Out, bool ObjectModel = false, - const std::vector *OriginExtents = nullptr) { + const std::vector *OriginExtents = nullptr, + const std::set *OutParameters = nullptr) { auto Collect = [&](const VExpr *Sub, SafetyChecks &Into) { collectSafety(Sub, FnMap, ValidExtents, PointerParams, Into, ObjectModel, - OriginExtents); + OriginExtents, OutParameters); }; if (!E) { addSafety(Out, ProofObligationKind::Unsupported, nullptr, SourceLocation(), @@ -2250,8 +2256,10 @@ collectSafety(const VExpr *E, const FunctionMap *FnMap, Collect(L->Ptr.get(), Out); addSafety(Out, ProofObligationKind::Dereference, nonNullSafety(L->Ptr.get(), L->Loc, ObjectModel), L->Loc); - addSafety(Out, ProofObligationKind::Initialization, - initializedSafety(L->Ptr.get(), L->Loc, ObjectModel), L->Loc); + addSafety( + Out, ProofObligationKind::Initialization, + initializedSafety(L->Ptr.get(), L->Loc, ObjectModel, OutParameters), + L->Loc); if (L->AccessCondition) addSafety(Out, ProofObligationKind::Bounds, cloneVExpr(L->AccessCondition.get()), L->Loc); @@ -3553,6 +3561,10 @@ class PassivizerImpl { std::vector ActiveValidExtents; std::set PointerParameterNames; std::set SourcePointerParameterNames; + /// The entry versions of the out-parameters, which are never reassigned: + /// a renamed address based on one is in storage whose initialization the + /// function tracks. + std::set OutParameterVersions; /// The objects of the pointer parameters, for origins: the declared /// extents, and one object of its pointee type (no length) for a /// parameter without one. @@ -4545,6 +4557,19 @@ class PassivizerImpl { Loc, VType::makeInt32(VIntMode::Math)); } + /// Whether the function tracks the initialization of the storage Ptr + /// addresses, source or renamed: local or dynamic storage, or an + /// out-parameter's. + bool tracksInitialization(const VExpr *Ptr) const { + if (hasPointerProvenance(Ptr)) + return true; + const VExpr *Base = pointerBase(Ptr); + if (!Base || Base->K != VExpr::Var) + return false; + const std::string &Name = static_cast(Base)->Name; + return Fn.OutParameters.count(Name) || OutParameterVersions.count(Name); + } + void collectModified(const VStmt &S, std::set &Out) const { switch (S.K) { case VStmt::Assign: @@ -4552,8 +4577,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())) + // A store to storage whose initialization is tracked initializes the + // cell. + if (tracksInitialization(static_cast(S).Ptr.get())) Out.insert(VInitializationHeapName); break; case VStmt::Allocate: { @@ -4616,6 +4642,13 @@ class PassivizerImpl { (!Callee->second->Modifies.empty() || hasImplicitHeapEffect(*Callee->second, FnMap))) Out.insert(VHeapName); + if (Callee != FnMap.end()) + for (unsigned I = 0; + I < C.Args.size() && I < Callee->second->Params.size(); ++I) + if (Callee->second->OutParameters.count( + Callee->second->Params[I].first) && + tracksInitialization(C.Args[I].get())) + Out.insert(VInitializationHeapName); break; } case VStmt::GhostBlock: @@ -4670,7 +4703,8 @@ class PassivizerImpl { SafetySource ? SafetySource : E, &FnMap, SafetySource ? &Fn.ValidExtents : &ActiveValidExtents, SafetySource ? &SourcePointerParameterNames : &PointerParameterNames, - Checks, Fn.ObjectModel, SafetySource ? &OriginObjects : nullptr); + Checks, Fn.ObjectModel, SafetySource ? &OriginObjects : nullptr, + SafetySource ? &Fn.OutParameters : &OutParameterVersions); if (MemoryChecks && !Fn.TotalExpressions) for (const VMemoryCheck &Check : *MemoryChecks) Checks.push_back({Check.Kind, cloneVExpr(Check.Cond.get())}); @@ -5015,13 +5049,17 @@ class PassivizerImpl { for (const auto &Param : Fn.Params) { std::string V0 = versionedName(Param.first); - OldState[Param.first] = - std::make_unique(V0, Param.second, SourceLocation()); + OldState[Param.first] = std::make_unique( + V0, Param.second, SourceLocation(), + Fn.IsConstructor && Param.first == "this" ? VConstructedObjectLifetime + : ""); Renames[Param.first] = V0; if (Param.second.Kind == VTypeKind::Ptr) { PointerParameterNames.insert(V0); SourcePointerParameterNames.insert(Param.first); } + if (Fn.OutParameters.count(Param.first)) + OutParameterVersions.insert(V0); } for (const VValidExtent &Extent : Fn.ValidExtents) OriginObjects.emplace_back(Extent.Base, Extent.PointerType, @@ -5188,7 +5226,7 @@ class PassivizerImpl { SafetyChecks Checks; collectSafety(Post, &FnMap, &Fn.ValidExtents, &SourcePointerParameterNames, Checks, Fn.ObjectModel, - &OriginObjects); + &OriginObjects, &Fn.OutParameters); if (!Fn.TotalExpressions && I < Fn.PostconditionChecks.size()) for (const VMemoryCheck &Check : Fn.PostconditionChecks[I]) Checks.push_back({Check.Kind, cloneVExpr(Check.Cond.get())}); @@ -5331,7 +5369,7 @@ class PassivizerImpl { /// In the object model a pointer without provenance is valid where it lies /// in one of the caller's objects or is a known valid object of its own, - /// and abstract storage is initialized. + /// and abstract storage is initialized, but for an out-parameter's. std::unique_ptr abstractValidity(std::unique_ptr E, const std::map &Renames) { @@ -5340,6 +5378,9 @@ class PassivizerImpl { switch (E->K) { case VExpr::UnaryOp: { auto *U = static_cast(E.get()); + if (U->Op == VUnaryOp::InitializedPtr && + tracksInitialization(U->Operand.get())) + return E; if ((U->Op == VUnaryOp::ValidPtr || U->Op == VUnaryOp::InitializedPtr) && !hasPointerProvenance(U->Operand.get())) { if (U->Op == VUnaryOp::InitializedPtr) @@ -5416,12 +5457,13 @@ class PassivizerImpl { Loc)}; } - /// A record in local or dynamic storage passed to a parameter that - /// addresses one: the generated validity clause names its first byte, and - /// the callee reads every leaf as valid and initialized storage. Each byte - /// up to its last belongs to the live allocation of its first when the - /// last does (an allocation's bytes are contiguous), and each leaf must be - /// initialized, which C++ does not require of an out-parameter. + /// A record in local or dynamic storage, or in an out-parameter's, passed + /// to a parameter that addresses one: the generated validity clause names + /// its first byte, and the callee reads every leaf as valid and + /// initialized storage. Each byte up to its last belongs to the live + /// allocation of its first when the last does (an allocation's bytes are + /// contiguous), and each leaf must be initialized unless the callee's + /// parameter is an out-parameter. void emitRecordActualChecks( PassiveProgram &P, const VFunction &Callee, const std::set &DynamicParams, @@ -5431,7 +5473,9 @@ class PassivizerImpl { return; for (const auto &[Name, Identity] : Callee.RecordParams) { auto Actual = ParamMap.find(Name); - if (!DynamicParams.count(Name) || Actual == ParamMap.end()) + const bool Dynamic = DynamicParams.count(Name); + if (Actual == ParamMap.end() || + !(Dynamic || tracksInitialization(Actual->second.get()))) continue; const auto Layout = llvm::find_if(Callee.Layouts, [&](const VObjectLayout &L) { @@ -5445,15 +5489,18 @@ class PassivizerImpl { std::to_string(Bytes), pointerOffsetType(), Loc), Loc); }; - emitPassive(P, PassiveStmt::Assert, - std::make_unique( - VUnaryOp::ValidPtr, Offset(Layout->SizeBytes - 1), - VType::makeBool(), Loc, - stateHeapName(Ctx, VAllocationHeapName, ""), - stateHeapName(Ctx, VLivenessHeapName, "")), - nullptr, Loc, ProofObligationKind::PointerValidity); - // A constructor's object is what it initializes. - if (Callee.IsConstructor && Name == "this") + if (Dynamic) + emitPassive(P, PassiveStmt::Assert, + std::make_unique( + VUnaryOp::ValidPtr, Offset(Layout->SizeBytes - 1), + VType::makeBool(), Loc, + stateHeapName(Ctx, VAllocationHeapName, ""), + stateHeapName(Ctx, VLivenessHeapName, "")), + nullptr, Loc, ProofObligationKind::PointerValidity); + // A constructor's object is what it initializes, and an out-parameter + // is written before it is read. + if ((Callee.IsConstructor && Name == "this") || + Callee.OutParameters.count(Name)) continue; std::vector Leaves; for (const VObjectLeaf &Leaf : Layout->Leaves) { @@ -6115,6 +6162,16 @@ class PassivizerImpl { havocFootprints(P, Renames, *Callee, ActualModifies, ActualCounts, ParamMap, Ctx, EntryHeap, HasImplicitHeapEffect, C.Loc); + // Storage the caller tracks, passed to an out-parameter, may be + // initialized by the call; what was initialized stays so. + const bool InitializesActuals = initializesActuals(*Callee, ParamMap); + if (InitializesActuals) { + const std::string Before = Renames[VInitializationHeapName]; + const std::string After = bump(VInitializationHeapName); + Renames[VInitializationHeapName] = After; + emitPassive(P, PassiveStmt::Assume, + initializationKept(Before, After, C.Loc), nullptr, 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) { @@ -6154,6 +6211,40 @@ class PassivizerImpl { P.Stmts[FirstPost]->PostClauses = P.Stmts.size() - FirstPost; P.Stmts[FirstPost]->CallLoc = C.Loc; } + // The storage a postcondition reads is initialized where it reads it, as + // the callee's exit checks of its definedness show: that is what an + // out-parameter gives the caller. + if (InitializesActuals) + for (const auto &Post : Callee->Postconditions) { + SafetyChecks Checks; + collectSafety(Post.get(), &FnMap, &Callee->ValidExtents, + &CalleePointerParams, Checks, Fn.ObjectModel, nullptr, + &Callee->OutParameters); + for (const SafetyCheck &Check : Checks) { + if (Check.Kind != ProofObligationKind::Initialization) + continue; + auto PS = std::make_unique(); + PS->K = PassiveStmt::Assume; + PS->Origin = "call:" + Callee->Name; + PS->Cond = rebaseSliceBinders( + substParams(Check.Cond.get(), PostParamMap, Ctx, EntryHeap, "", + {}, &ParamMap)); + P.Stmts.push_back(std::move(PS)); + } + } + } + + /// Whether a call of Callee may initialize storage the caller tracks: an + /// out-parameter's argument is local or dynamic storage, or the caller's + /// own out-parameter's. + bool initializesActuals( + const VFunction &Callee, + const std::map> &ParamMap) const { + return llvm::any_of(Callee.OutParameters, [&](const std::string &Name) { + auto Actual = ParamMap.find(Name); + return Actual != ParamMap.end() && + tracksInitialization(Actual->second.get()); + }); } // The origin of the assumptions a statement makes, before its parts name @@ -6345,7 +6436,7 @@ class PassivizerImpl { if (PointerCell) StoredPointerCells.push_back({std::move(PointerCell), StoredPointerType, cloneVExpr(Active.get())}); - if (hasPointerProvenance(St.Ptr.get())) + if (tracksInitialization(St.Ptr.get())) updateHeap(P, Renames, VInitializationHeapName, cloneExpr(St.Ptr.get(), Ctx), makeBoolLiteral(true, St.Loc), Active.get(), St.Loc); diff --git a/clang/test/Verify/suite/constructors.cpp b/clang/test/Verify/suite/constructors.cpp index c33a1ed441..3a46c95158 100644 --- a/clang/test/Verify/suite/constructors.cpp +++ b/clang/test/Verify/suite/constructors.cpp @@ -139,9 +139,9 @@ int holder_sum() } // 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. +// A member function that writes its object before reading it may be called +// before any member is initialized: its object is an out-parameter, written +// on every path, so the call initializes it. struct Resets { Resets() cppverify::post(v == 0) @@ -158,7 +158,28 @@ struct Resets { int v; }; -// CHECK-DAG: Unresolved: Resets::Resets [backend=z3] [reason=construct.unsupported] +// CHECK-DAG: Verified: Resets::Resets [backend=z3] + +// One that may read its object first is unsupported there, as any callee +// that may read storage not initialized yet. +struct Keeps { + Keeps() + cppverify::post(v == 1) + { + keep(); + v = 1; + } + + void keep() + cppverify::modifies(v) + cppverify::post(v == cppverify::old(v)) + { + v = v + 0; + } + + int v; +}; +// CHECK-DAG: Unresolved: Keeps::Keeps [backend=z3] [reason=construct.unsupported] // A loop initializes an array member, as an invariant states. struct Ring { diff --git a/clang/test/Verify/suite/local_record_arguments.cpp b/clang/test/Verify/suite/local_record_arguments.cpp index e43baefa16..440e4be597 100644 --- a/clang/test/Verify/suite/local_record_arguments.cpp +++ b/clang/test/Verify/suite/local_record_arguments.cpp @@ -370,8 +370,8 @@ int same_local() } // CHECK-DAG: error: verification failed: same_local [{{.*}}::aliasing@[[@LINE-3]]:3] -// Every field must be initialized: the callee reads its record as -// initialized storage, which C++ does not require of an out-parameter. +// A callee that writes its record before reading it needs none of it +// initialized: c.limit never is. One that may read it needs every field. void set_n(Counter &c) cppverify::modifies(c.n) cppverify::post(c.n == 1) @@ -387,7 +387,22 @@ int out_parameter() set_n(c); return c.n; } -// CHECK-DAG: [[@LINE-3]]:3: Unresolved: out_parameter [backend=z3] [reason=construct.unsupported] (the verifier cannot model a construct here: binding a reference or pointer parameter to storage that is not initialized, since the callee is verified as reading initialized storage) +// CHECK-DAG: Verified: out_parameter [backend=z3] + +int get_n(const Counter &c) + cppverify::post(cppverify::result == c.n) +{ + return c.n; +} + +int partly_initialized() + cppverify::post(cppverify::result == 0) +{ + Counter c; + c.n = 0; + return get_n(c); +} +// CHECK-DAG: [[@LINE-2]]:3: Unresolved: partly_initialized [backend=z3] [reason=construct.unsupported] (the verifier cannot model a construct here: binding a reference or pointer parameter to storage that is not initialized, which the callee may read before writing it) // A callee that keeps the address: in memory, or by returning it. struct Node { diff --git a/clang/test/Verify/suite/local_reference_lowering.cpp b/clang/test/Verify/suite/local_reference_lowering.cpp index 55e7f8bfae..066f0ad056 100644 --- a/clang/test/Verify/suite/local_reference_lowering.cpp +++ b/clang/test/Verify/suite/local_reference_lowering.cpp @@ -43,11 +43,13 @@ int local_reference_lowering(int value) // PASSIVE: heap_store // PASSIVE: local_1 // PASSIVE: valid_ptr -// PASSIVE: initialized_ptr // PASSIVE: alias_1 // PASSIVE: __cppverify_reference_provenance_1_1 // PASSIVE: __cppverify_stack_provenance_1_1 // PASSIVE: heap_store +// PASSIVE: forall __init_address +// PASSIVE: initialized_ptr +// PASSIVE-NEXT: alias_1 // PASSIVE: load // PASSIVE: local_1 // PASSIVE: result diff --git a/clang/test/Verify/suite/out_parameters.cpp b/clang/test/Verify/suite/out_parameters.cpp index 0846a54bb0..4a96705e4b 100644 --- a/clang/test/Verify/suite/out_parameters.cpp +++ b/clang/test/Verify/suite/out_parameters.cpp @@ -1,56 +1,97 @@ -// RUN: not %cpp-verify %s -- 2>&1 | FileCheck %s +// RUN: not %cpp-verify --jobs=1 %s -- -Wno-tautological-compare > %t 2>&1 +// RUN: FileCheck %s < %t +// RUN: FileCheck %s --check-prefix=SOUND < %t +// RUN: %cpp-verify --lower-only --dump-ir=1 %s -- -Wno-tautological-compare 2>&1 | FileCheck %s --check-prefix=VCR +// RUN: not %cpp-verify --jobs=1 --no-check-ub %s -- -Wno-tautological-compare 2>&1 | FileCheck %s --check-prefix=NOUB // Binding a reference or passing a pointer reads nothing ([dcl.init.ref], // [conv.lval]); only reading an indeterminate value is undefined -// ([basic.indet]). A local's initialization is checked where it is read. -// A function is still verified as reading its pointer and reference -// parameters' storage, and its callers its pointer result's, as initialized, -// so a call or return that cannot show it is unsupported, not a failure. +// ([basic.indet]). A parameter whose storage the body never reads before +// writing it is an out-parameter: callers may pass storage that is not +// initialized, the body's reads of it are checked against what it wrote, +// and the leaves it writes on every path are initialized when it returns. +// A parameter the body may read first keeps the rule that its storage is +// initialized, and a call that cannot show that is unsupported. +// +// No proof here holds only because no execution reaches its end. +// SOUND-NOT: vacuous + +namespace cv = cppverify; + +struct Pair { + int a; + int b; +}; void init_ref(int &r) - cppverify::modifies(r) - cppverify::post(r == 0) + cv::modifies(r) + cv::post(r == 0) { r = 0; } // CHECK: Verified: init_ref +// NOUB: Verified: init_ref +// VCR-LABEL: fn init_ref +// VCR-NEXT: param r out +// VCR-NEXT: pre +// VCR-NEXT: && +// VCR-NEXT: ! +// VCR-NEXT: == +// VCR-NEXT: r +// VCR-NEXT: 0 +// VCR-NEXT: valid_ptr +// VCR-NEXT: r +// VCR-NEXT: post +// VCR-NEXT: == +// VCR-NEXT: load +// VCR-NEXT: r +// VCR-NEXT: 0 +// VCR-NEXT: initialized_ptr +// VCR-NEXT: r +// VCR-NEXT: modifies void init_ptr(int *p) - cppverify::pre(p != nullptr) - cppverify::modifies(*p) - cppverify::post(*p == 0) + cv::pre(p != nullptr) + cv::modifies(*p) + cv::post(*p == 0) { *p = 0; } // CHECK: Verified: init_ptr +// VCR-LABEL: fn init_ptr +// VCR-NEXT: param p out int read_ref(const int &r) - cppverify::post(cppverify::result == r) + cv::post(cv::result == r) { return r; } // CHECK: Verified: read_ref +// VCR-LABEL: fn read_ref +// VCR-NEXT: param r{{$}} +// VCR: initialized_ptr int scalar_out() - cppverify::post(cppverify::result == 0) + cv::post(cv::result == 0) { int a; init_ref(a); return a; } -// CHECK: Unresolved: scalar_out {{.*}}[reason=construct.unsupported] (the verifier cannot model a construct here: binding a reference or pointer parameter to storage that is not initialized, since the callee is verified as reading initialized storage) +// CHECK: Verified: scalar_out int array_out() - cppverify::post(cppverify::result == 0) + cv::post(cv::result == 0) { int a[2]; init_ref(a[0]); return a[0]; } -// CHECK: Unresolved: array_out {{.*}}[reason=construct.unsupported] +// CHECK: Verified: array_out +// NOUB: Verified: array_out int heap_out() - cppverify::post(cppverify::result == 0) + cv::post(cv::result == 0) { int *p = new int; init_ptr(p); @@ -58,10 +99,11 @@ int heap_out() delete p; return v; } -// CHECK: Unresolved: heap_out {{.*}}[reason=construct.unsupported] +// CHECK: Verified: heap_out +// NOUB: Verified: heap_out int initialized_argument() - cppverify::post(cppverify::result == 0) + cv::post(cv::result == 0) { int a = 7; init_ref(a); @@ -70,7 +112,7 @@ int initialized_argument() // CHECK: Verified: initialized_argument int written_through_local_reference() - cppverify::post(cppverify::result == 3) + cv::post(cv::result == 3) { int a; int &r = a; @@ -80,7 +122,7 @@ int written_through_local_reference() // CHECK: Verified: written_through_local_reference int read_before_written() - cppverify::post(cppverify::result == 3) + cv::post(cv::result == 3) { int a; int &r = a; @@ -90,7 +132,7 @@ int read_before_written() // CHECK: error: verification failed: read_before_written {{.*}}initialization@[[@LINE-3]]:3 int *fresh() - cppverify::post(cppverify::result != nullptr) + cv::post(cv::result != nullptr) { int *p = new int; return p; @@ -98,11 +140,534 @@ int *fresh() // CHECK: Unresolved: fresh {{.*}}[reason=construct.unsupported] (the verifier cannot model a construct here: returning a pointer to storage that is not initialized, since callers read a returned pointer's storage as initialized) // The callee reads the indeterminate value, which is undefined, but its -// verification cannot say that it reads before it writes: unsupported too. +// verification cannot say that it reads before it writes: unsupported. int reads_uninitialized() - cppverify::post(cppverify::result == 0) + cv::post(cv::result == 0) { int a; return read_ref(a); } -// CHECK: Unresolved: reads_uninitialized {{.*}}[reason=construct.unsupported] +// CHECK: Unresolved: reads_uninitialized {{.*}}[reason=construct.unsupported] (the verifier cannot model a construct here: binding a reference or pointer parameter to storage that is not initialized, which the callee may read before writing it) + +// Written on every path, with no postcondition about it: initialized after +// the call, its value unknown. +void set_some(int &x) + cv::modifies(x) +{ + x = 1; +} +// CHECK: Verified: set_some +// VCR-LABEL: fn set_some +// VCR-NEXT: param x out +// VCR: post +// VCR-NEXT: initialized_ptr +// VCR-NEXT: x +// VCR-NEXT: modifies + +int reads_what_was_set() + cv::post(cv::result == 0) +{ + int a[1]; + set_some(a[0]); + int v = a[0]; + return 0; +} +// CHECK: Verified: reads_what_was_set +// NOUB: Verified: reads_what_was_set + +// Written on one path: the postcondition says on which. +bool try_get(int &out, bool ok) + cv::modifies(out) + cv::post(!cv::result || out == 5) +{ + if (!ok) + return false; + out = 5; + return true; +} +// CHECK: Verified: try_get +// VCR-LABEL: fn try_get +// VCR-NEXT: param out out +// VCR-NEXT: param ok +// VCR: post +// VCR-NOT: initialized_ptr +// VCR: modifies + +int got(bool ok) + cv::post(cv::result == 5 || cv::result == 0) +{ + int a[1]; + bool found = try_get(a[0], ok); + if (found) + return a[0]; + return 0; +} +// CHECK: Verified: got +// NOUB: Verified: got + +int reads_after_failed_get() + cv::post(cv::result == 0) +{ + int a[1]; + try_get(a[0], false); + return a[0]; +} +// CHECK: error: verification failed: reads_after_failed_get {{.*}}initialization@[[@LINE-2]]:3 +// NOUB: error: verification failed: reads_after_failed_get {{.*}}initialization@[[@LINE-3]]:3 + +// Written, then read: still an out-parameter. +void write_then_update(int &x) + cv::modifies(x) + cv::post(x == 1) +{ + x = 0; + x = x + 1; +} +// CHECK: Verified: write_then_update +// VCR-LABEL: fn write_then_update +// VCR-NEXT: param x out + +int updated() + cv::post(cv::result == 1) +{ + int a[1]; + write_then_update(a[0]); + return a[0]; +} +// CHECK: Verified: updated + +// Read on a path before it is written: an input. +void reset_or_bump(int &x, bool c) + cv::pre(c || x < 100) + cv::modifies(x) + cv::post(x <= 100) +{ + if (c) + x = 0; + x = x + 1; +} +// CHECK: Verified: reset_or_bump +// VCR-LABEL: fn reset_or_bump +// VCR-NEXT: param x{{$}} + +int reset_uninitialized() + cv::post(cv::result == 1) +{ + int a[1]; + reset_or_bump(a[0], true); + return a[0]; +} +// CHECK: Unresolved: reset_uninitialized {{.*}}[reason=construct.unsupported] + +// The contract reads the entry value: an input. +void clamp_nonnegative(int &x) + cv::pre(x >= -5) + cv::modifies(x) + cv::post(x >= 0) +{ + x = 0; +} +// CHECK: Verified: clamp_nonnegative +// VCR-LABEL: fn clamp_nonnegative +// VCR-NEXT: param x{{$}} + +void zero_if(int &x, bool c) + cv::modifies(x) + cv::post(c ? x == 0 : x == cv::old(x)) +{ + if (c) + x = 0; +} +// CHECK: Verified: zero_if +// VCR-LABEL: fn zero_if +// VCR-NEXT: param x{{$}} + +// Passed on: what the callee writes on every path is written here. +void set_twice(int &r) + cv::modifies(r) + cv::post(r == 2) +{ + set_some(r); + int seen = r; + r = 2; +} +// CHECK: Verified: set_twice +// VCR-LABEL: fn set_twice +// VCR-NEXT: param r out + +int set_through() + cv::post(cv::result == 2) +{ + int a[1]; + set_twice(a[0]); + return a[0]; +} +// CHECK: Verified: set_through + +// Written, then passed to a callee that reads it; read by a callee first. +void write_then_read(int &x) + cv::modifies(x) + cv::post(x == 4) +{ + x = 4; + int v = read_ref(x); +} +// CHECK: Verified: write_then_read +// VCR-LABEL: fn write_then_read +// VCR-NEXT: param x out + +void read_then_write(int &x) + cv::modifies(x) + cv::post(x == 4) +{ + int v = read_ref(x); + x = 4; +} +// CHECK: Verified: read_then_write +// VCR-LABEL: fn read_then_write +// VCR-NEXT: param x{{$}} + +[[cppverify::trusted]] void external_set(int &x) + cv::modifies(x) + cv::post(x == 1); +// CHECK: Trusted: external_set + +// A callee without a verified body may read what it receives: an input. +void through_external(int &x) + cv::modifies(x) + cv::post(x == 1) +{ + external_set(x); +} +// CHECK: Verified: through_external +// VCR-LABEL: fn through_external +// VCR-NEXT: param x{{$}} + +// A record written field by field. +void make_pair(Pair &p) + cv::modifies(p) + cv::post(p.a == 1) +{ + p.a = 1; + p.b = 2; +} +// CHECK: Verified: make_pair +// NOUB: Verified: make_pair +// VCR-LABEL: fn make_pair +// VCR-NEXT: param p out +// VCR: post +// VCR: initialized_ptr +// VCR-NEXT: p +// VCR-NEXT: initialized_ptr +// VCR-NEXT: + +// VCR-NEXT: p +// VCR-NEXT: 4 + +int made() + cv::post(cv::result == 1) +{ + Pair p; + make_pair(p); + int b = p.b; + return p.a; +} +// CHECK: Verified: made + +// Its fields bound to a callee's out-parameter, one after the other. +void make_by_parts(Pair &p) + cv::modifies(p) + cv::post(p.a == 0 && p.b == 0) +{ + init_ref(p.a); + init_ref(p.b); +} +// CHECK: Verified: make_by_parts +// VCR-LABEL: fn make_by_parts +// VCR-NEXT: param p out + +int made_by_parts() + cv::post(cv::result == 0) +{ + Pair p; + make_by_parts(p); + return p.a + p.b; +} +// CHECK: Verified: made_by_parts + +// One field written, then the record passed to a callee that reads both: +// an input. +int second_of(const Pair &q) + cv::post(cv::result == q.b) +{ + return q.b; +} +// CHECK: Verified: second_of + +void write_a_then_read(Pair &p) + cv::modifies(p) + cv::post(p.a == 1 && p.b == 2) +{ + p.a = 1; + int b = second_of(p); + p.b = 2; +} +// CHECK: Verified: write_a_then_read +// VCR-LABEL: fn write_a_then_read +// VCR-NEXT: param p{{$}} + +void make_first(Pair &p) + cv::modifies(p) + cv::post(p.a == 1) +{ + p.a = 1; +} +// CHECK: Verified: make_first + +int reads_unmade() + cv::post(cv::result == 1) +{ + Pair p; + make_first(p); + return p.b; +} +// CHECK: error: verification failed: reads_unmade {{.*}}initialization@[[@LINE-2]]:3 + +// A postcondition about storage the function never writes speaks of the +// caller's values: an input, initialized at entry. +void untouched(int &x) + cv::modifies(x) + cv::post(x == x) +{ +} +// CHECK: Verified: untouched +// VCR-LABEL: fn untouched +// VCR-NEXT: param x{{$}} + +// One that it writes on a path: a read of what it wrote. +void set_if(int &x, bool c) + cv::modifies(x) + cv::post(x == 1) +{ + if (c) + x = 1; +} +// CHECK: error: verification failed: set_if {{.*}}initialization@[[@LINE-5]]:14 +// NOUB: error: verification failed: set_if {{.*}}initialization@[[@LINE-6]]:14 + +// A loop writes on no path known before it runs. +void zero_each(int &x, int n) + cv::pre(n >= 0) + cv::modifies(x) +{ + for (int i = 0; i < n; i = i + 1) + cv::invariant(0 <= i && i <= n) + cv::decreases(n - i) + { + x = 0; + } +} +// CHECK: Verified: zero_each +// VCR-LABEL: fn zero_each +// VCR-NEXT: param x out +// VCR-NEXT: param n +// VCR: post +// VCR-NEXT: modifies + +int maybe_zeroed() + cv::post(cv::result == 0) +{ + int a[1]; + zero_each(a[0], 0); + return a[0]; +} +// CHECK: error: verification failed: maybe_zeroed {{.*}}initialization@[[@LINE-2]]:3 + +// Calls in a loop: each keeps what was initialized before it. +int init_in_loop() + cv::post(cv::result == 0) +{ + int a[1]; + init_ref(a[0]); + for (int i = 0; i < 3; i = i + 1) + cv::invariant(0 <= i && i <= 3 && a[0] == 0) + cv::decreases(3 - i) + { + init_ref(a[0]); + } + return a[0]; +} +// CHECK: Verified: init_in_loop + +// What a call in one iteration initializes, the next reads. +int init_once_in_loop() + cv::post(cv::result == 0) +{ + int a[1]; + int s = 0; + for (int i = 0; i < 3; i = i + 1) + cv::invariant(0 <= i && i <= 3 && s == 0) + cv::invariant(i == 0 || a[0] == 0) + cv::decreases(3 - i) + { + if (i == 0) + init_ref(a[0]); + s = s + a[0]; + } + return s; +} +// CHECK: Verified: init_once_in_loop + +int init_in_loop_only(int n) + cv::pre(0 <= n && n <= 3) + cv::post(cv::result == 0) +{ + int a[1]; + for (int i = 0; i < n; i = i + 1) + cv::invariant(0 <= i && i <= n) + cv::decreases(n - i) + { + init_ref(a[0]); + } + return a[0]; +} +// CHECK: error: verification failed: init_in_loop_only {{.*}}initialization@[[@LINE-2]]:3 + +void zero_rec(int &x, int n) + cv::pre(n >= 0) + cv::modifies(x) + cv::post(x == 0) + cv::decreases(n) +{ + if (n == 0) { + x = 0; + return; + } + zero_rec(x, n - 1); +} +// CHECK: Verified: zero_rec +// VCR-LABEL: fn zero_rec +// VCR-NEXT: param x out + +// A null test reads nothing. +void set_if_given(int *p) + cv::modifies(*p) + cv::post(p == nullptr || *p == 7) +{ + if (p) + *p = 7; +} +// CHECK: Verified: set_if_given +// VCR-LABEL: fn set_if_given +// VCR-NEXT: param p out + +int given() + cv::post(cv::result == 7) +{ + int *p = new int; + set_if_given(p); + int v = *p; + delete p; + return v; +} +// CHECK: Verified: given + +// A copy of the pointer is a use of it: an input. +void through_copy(int *p) + cv::pre(p != nullptr) + cv::modifies(*p) + cv::post(*p == 3) +{ + int *q = p; + *q = 3; +} +// CHECK: Verified: through_copy +// VCR-LABEL: fn through_copy +// VCR-NEXT: param p{{$}} + +// Through a copy of the pointer, a read is not seen as one: an input, so a +// caller cannot pass a record that is not initialized. +void through_alias(Pair *p) + cv::pre(p != nullptr) + cv::modifies(*p) + cv::post(p->a == 1) +{ + Pair *q = p; + int seen = q->b; + p->a = 1; + p->b = 2; +} +// CHECK: Verified: through_alias +// VCR-LABEL: fn through_alias +// VCR-NEXT: param p{{$}} + +int alias_reads_garbage() + cv::post(cv::result == 1) +{ + Pair x; + through_alias(&x); + return x.a; +} +// CHECK: Unresolved: alias_reads_garbage {{.*}}[reason=construct.unsupported] + +// A loop that fills an array, and a function that passes its array on. +void fill(int *p, int n) + cv::pre(n >= 0 && cv::valid(p, n)) + cv::modifies(p[0 : n]) + cv::post(cv::forall(k, 0, n, p[k] == 0)) +{ + for (int i = 0; i < n; i = i + 1) + cv::invariant(0 <= i && i <= n) + cv::invariant(cv::forall(k, 0, i, p[k] == 0)) + cv::decreases(n - i) + { + p[i] = 0; + } +} +// CHECK: Verified: fill +// VCR-LABEL: fn fill +// VCR-NEXT: param p out + +void fill_four(int *b) + cv::pre(cv::valid(b, 4)) + cv::modifies(b[0 : 4]) + cv::post(cv::forall(k, 0, 4, b[k] == 0)) +{ + fill(b, 4); +} +// CHECK: Verified: fill_four + +void fill_three(int *b) + cv::pre(cv::valid(b, 4)) + cv::modifies(b[0 : 4]) + cv::post(cv::forall(k, 0, 4, b[k] == 0)) +{ + fill(b, 3); +} +// CHECK: error: verification failed: fill_three {{.*}}initialization@[[@LINE-4]]:12 + +// A member function that writes its object. +struct Point { + int x; + int y; + void reset() + cv::modifies(*this) + { + x = 0; + y = 0; + } +}; +// CHECK: Verified: Point::reset +// NOUB: Verified: Point::reset +// VCR-LABEL: fn Point::reset +// VCR-NEXT: param this out + +int reset_point() + cv::post(cv::result == 0) +{ + Point p; + p.reset(); + int y = p.y; + return 0; +} +// CHECK: Verified: reset_point + diff --git a/clang/test/Verify/suite/region_frames.cpp b/clang/test/Verify/suite/region_frames.cpp index a64103cf23..fbfbf259c6 100644 --- a/clang/test/Verify/suite/region_frames.cpp +++ b/clang/test/Verify/suite/region_frames.cpp @@ -37,6 +37,9 @@ void zero_tail(int *p, int n, int lo, const int *other) } // CHECK-DAG: Verified: zero_tail +// The call writes only the slice; p, read nowhere but by the +// postcondition, is an out-parameter, so the cell before the slice may hold +// no value at all. void claims_too_much(int *p, int n, int lo) cppverify::pre(valid(p, n) && n >= 2 && n <= 1000 && 1 <= lo && lo < n) cppverify::modifies(*p) @@ -44,7 +47,7 @@ void claims_too_much(int *p, int n, int lo) { zero(p + lo, n - lo); } -// CHECK-DAG: error: verification failed: claims_too_much [{{.*}}::postcondition@ +// CHECK-DAG: error: verification failed: claims_too_much [{{.*}}::initialization@ // A function writing a range of its buffer. void zero_from(int *p, int n, int lo) diff --git a/clang/test/Verify/suite/shared_logic_terms.test b/clang/test/Verify/suite/shared_logic_terms.test index 53b963ce24..c862c53d6b 100644 --- a/clang/test/Verify/suite/shared_logic_terms.test +++ b/clang/test/Verify/suite/shared_logic_terms.test @@ -14,7 +14,7 @@ # RUN: | FileCheck %s --check-prefix=FIB # # A subterm that several goals share is simplified once; its rewrites still -# count once for each place, as when each was a copy (main printed 265 here). +# count once for each place, as when each was a copy. # RUN: %cpp-verify --lower-only --jobs=1 --dump-ir=3 \ # RUN: %S/backend_counterexample_trace.cpp -- 2>&1 | FileCheck %s --check-prefix=REWRITES # @@ -30,6 +30,6 @@ ULEB: Lowered: roundtrip_uleb128 FIB: Lowered: iterative_fibonacci REWRITES: vc set_value -REWRITES: simplification nodes 3632 -> 1252, rewrites 265, functions-removed 0 +REWRITES: simplification nodes 4850 -> 1750, rewrites 366, functions-removed 0 LETS: statements that bind a let name twice: 0 diff --git a/clang/test/Verify/suite/std_min_max.cpp b/clang/test/Verify/suite/std_min_max.cpp new file mode 100644 index 0000000000..b97cf14c83 --- /dev/null +++ b/clang/test/Verify/suite/std_min_max.cpp @@ -0,0 +1,149 @@ +// RUN: not %cpp-verify --jobs=1 %s -- > %t 2>&1 +// RUN: FileCheck %s < %t +// RUN: FileCheck %s --check-prefix=SOUND < %t +// +// std::min and std::max of two integers mean what the standard says they +// mean, whatever the library: max(a, b) is a unless a < b, and min(a, b) is +// a unless b < a. The library's other functions are not modeled, and a +// constexpr helper's references to const scalars stand for their values. +// +// No proof here holds only because no execution reaches its end. +// SOUND-NOT: vacuous + +#include + +int clamp3(int x) + cppverify::post(cppverify::result == std::max(x, 3)) +{ + return x < 3 ? 3 : x; +} +// CHECK-DAG: Verified: clamp3 [backend=z3] + +int lower(int a, int b) + cppverify::post(cppverify::result == std::min(a, b)) + cppverify::post(cppverify::result <= a && cppverify::result <= b) +{ + int m = std::min(a, b); + return m; +} +// CHECK-DAG: Verified: lower [backend=z3] + +// The first argument when they are equal: std::max(a, b) is a, not b. +unsigned long widest(unsigned long a, unsigned long b) + cppverify::post(cppverify::result >= a && cppverify::result >= b) +{ + unsigned long w = std::max(a, b); + return w; +} +// CHECK-DAG: Verified: widest [backend=z3] + +int wrong(int a, int b) + cppverify::post(cppverify::result == std::max(a, b)) +{ + return std::min(a, b); +} +// CHECK-DAG: error: verification failed: wrong [{{.*}}::postcondition@[[@LINE-4]] + +int clamped(int x) + cppverify::post(cppverify::result == std::clamp(x, 0, 9)) +{ + return x < 0 ? 0 : (x > 9 ? 9 : x); +} +// CHECK-DAG: error: clamped: std::clamp is not modeled: of the standard library, the verifier knows std::min and std::max of two integers + +template +constexpr const T &mymax(const T &a, const T &b) { return a < b ? b : a; } + +int mine(int x) + cppverify::post(cppverify::result == mymax(x, 3)) +{ + return x < 3 ? 3 : x; +} +// CHECK-DAG: Verified: constexpr spec axiom: mymax +// CHECK-DAG: Verified: mine [backend=z3] + +constexpr int first(const int *p) { return p[0]; } + +int reads(const int *p) + cppverify::pre(cppverify::valid(p, 1)) + cppverify::post(cppverify::result == first(p)) +{ + return p[0]; +} +// CHECK-DAG: error: first: a constexpr function read as a spec cannot read memory through a pointer or an array +// CHECK-DAG: Unresolved: reads [reason=construct.unsupported] (relies on first, which uses a construct the verifier does not support) + +long widened(int x) + cppverify::post(cppverify::result == std::max(x, 3L)) + cppverify::post(cppverify::result >= 3) +{ + long w = std::max(x, 3L); + return w; +} +// CHECK-DAG: Verified: widened [backend=z3] + +int above(int a, int b) + cppverify::pre(a < 1000 && b < 1000) + cppverify::post(cppverify::result > a && cppverify::result > b) +{ + return std::max(a, b) + 1; +} +// CHECK-DAG: Verified: above [backend=z3] + +enum Level { Low, Mid, High }; + +Level highest(Level a, Level b) + cppverify::post(cppverify::result >= a && cppverify::result >= b) +{ + Level h = std::max(a, b); + return h; +} +// CHECK-DAG: Verified: highest [backend=z3] + +cppverify::spec int spread(int a, int b) { return std::max(a, b) - std::min(a, b); } + +int distance(int a, int b) + cppverify::pre(-1000 < a && a < 1000 && -1000 < b && b < 1000) + cppverify::post(cppverify::result == spread(a, b)) +{ + return a < b ? b - a : a - b; +} +// CHECK-DAG: Verified: spec axiom: spread +// CHECK-DAG: Verified: distance [backend=z3] + +// A reference to the result is not a value: it fails closed. +int bound(int a, int b) + cppverify::post(true) +{ + const int &r = std::max(a, b); + return r; +} +// CHECK-DAG: error: bound: local references require a supported direct lvalue + +// Of a class, std::max compares with the class's own operator<, which the +// model does not know. +struct Version { + int v; + constexpr bool operator<(const Version &o) const { return v < o.v; } +}; + +int newer(Version a, Version b) + cppverify::post(cppverify::result == std::max(a, b).v) +{ + return a.v < b.v ? b.v : a.v; +} +// CHECK-DAG: error: newer: std::max is not modeled: of the standard library, the verifier knows std::min and std::max of two integers + +// A reference the helper writes through is no value. +constexpr int bumped(int &x) { + x = x + 1; + return x; +} + +int bumps(int x) + cppverify::post(cppverify::result == bumped(x)) +{ + return x + 1; +} +// CHECK-DAG: error: bumped: unsupported C++ type in verification: int & +// CHECK-DAG: Unresolved: bumps [reason=construct.unsupported] (relies on bumped, which uses a construct the verifier does not support) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 496b8b0b85..5ee63626bd 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -253,11 +253,14 @@ scope and `this`, as its trailing requires-clause does. 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. +`this` the lifetime companion `VConstructedObjectLifetime` +(`__cppverify_constructed_lifetime`, every `CXXThisExpr`, and the entry +state's `this` in `PassivizerImpl::enter`, so the frame `*this` and the +`this` passed to a member function are one object), so its accesses are +those of local storage, initialization checked, and generates the +precondition that each leaf of `*this` and its last byte are 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 @@ -358,6 +361,19 @@ collected from its template only); `isInstantiated` decides the warning, from a function template's specializations or the instantiated members of the class's. +**std::min and std::max:** `stdMinOrMax` recognizes the two-argument +`std::min` and `std::max` of a const integer, enumeration, or `bool` +reference (not the overloads with a comparison or an initializer list), and +`convertMinOrMax` lowers a call to a `VConditionalExpr` over the converted +arguments, before a call becomes a spec application; any other non-constant +call of a `constexpr` function of `std` is a conversion error. In +`convertConstexprSpec`, `findUnsupportedType`'s +`ConstScalarReferencesAreValues` makes a reference to a const integer its +referent (`constScalarReferent`), as the parameter's and the result's +types, and the parameters in `ValueReferences` are read as values; a +function that cannot be lifted returns a placeholder that the lifting loop +marks unsupported, so `SpecDependencies` name it. + **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 @@ -490,6 +506,30 @@ VFunction = - `freshOwnedReturn` is a derived VCR effect, never a trusted contract claim. `Ownership.cpp` computes it by a conservative acyclic path analysis and cloning, loop unrolling, dumps, and every backend preserve it. +- `outParameters` (`VFunction::OutParameters`, printed `param p out`) is + derived the same way, by `inferOutParameters` + (`Transform/OutParameters.cpp`), which the driver runs on the converted + functions after `inferFreshOwnedReturns`. Per pointer or reference + parameter of a function with a verified body, a walk keeps the byte + offsets from the parameter written on every path (`Written`: an `if` + joins by intersection, a loop's body starts from what was written before + it and adds nothing after it, a `return` records the exit state) and + rejects a read of an offset not written, a read at a computed offset, any + other use of the pointer (a null test, `valid_ptr`, and address steps + excepted), a call passing it to a callee parameter that is not an + out-parameter whose leaves (`pointeeLeaves`, the record layout's) are not + all written or that has an extent, and an entry-state read in a clause + (`readsStorage`: preconditions, recommends, decreases, behaviors, field + parameters, footprint counts, extents, `old`). Postconditions, invariants, + and checks count only when the parameter is never written + (`WritesSomewhere`). Writes are a least fixpoint over the call graph + (a call adds the callee's writes for its formal at the argument's + offset), out-parameters a greatest one. For each out-parameter the pass + drops `initialized_ptr` from the generated validity precondition + (`withoutInitialization`), removes the converter's subobject binding + pair (an `initialization` assert of the object, an assume of the part's + initialization), and adds `initialized_ptr(p + offset)` postconditions of + kind `initialization` for the leaves written at every exit. - `identity` includes the canonical signature, so overloads with the same source spelling remain distinct through modular calls and SMT symbols. - `cppverify::aliases` empty means the implicit non-aliasing precondition applies to every pair of distinct pointer/reference parameters of which at least one is mutable. @@ -737,6 +777,25 @@ assume(Q[Result := y, Old(params) := args]); cell, materializes one disjoint initialized scalar object, then assumes the ordinary postconditions against that new heap. +**Out-parameters.** `PassivizerImpl::tracksInitialization(ptr)` holds for a +pointer with provenance and for one based on an out-parameter, by its source +name or its entry version (`OutParameterVersions`; an out-parameter is never +reassigned). A store through such a pointer sets its initialization bit, a +loop that stores through one counts the initialization heap as modified (so +its head keeps what was initialized, `initializationKept`, and assumes the +invariants' definedness), `collectSafety` checks a load based on an +out-parameter with `initialized_ptr` at its exact address +(`initializedSafety` with the out-parameters, in and outside the object +model), and `abstractValidity` keeps `initialized_ptr` on tracked storage +instead of taking it as true. At a call, `initializesActuals` asks whether +an out-parameter's argument is tracked in the caller; then, after the +footprints are havocked, the initialization heap gets a fresh version that +keeps every initialized address, the postconditions are assumed (with the +generated `initialized_ptr` ones), and each postcondition's `initialization` +checks, built with the callee's out-parameters and substituted at the +arguments, are assumed after them with the call's origin. `collectModified` +counts such a call in a loop as modifying the initialization heap. + **Contract well-formedness.** Every contract clause must be defined where it is evaluated, as Dafny's per-method `CheckWellFormed$$f` procedure requires. Its definedness checks are the core ones (`collectSafety`) and, under @@ -2596,9 +2655,11 @@ body; re-entering a scan through recursion assumes it holds. Offsets, steps, comparisons, conversions to integers, spec arguments, and ghost reads are admitted. At the call `emitRecordActualChecks` asserts the validity of the record's last byte (with the generated clause's first, the record lies in -one live allocation) and the initialization of every leaf of the callee's -layout, enumerated (an automatic object has at most 256 bytes), as an -`unsupported` obligation with the out-parameter note. `havocFootprints` +one live allocation) and, unless the callee's parameter is an out-parameter, +the initialization of every leaf of the callee's layout, enumerated (an +automatic object has at most 256 bytes), as an `unsupported` obligation with +the out-parameter note; for the caller's own out-parameter passed to an +input, only the leaves. `havocFootprints` frames a footprint rooted at such a parameter by its bytes through `footprintBytes`, never as the exact first cell the scalar rule uses. The frame check of the caller accepts the callee's footprints in its own diff --git a/docs/DESIGN.md b/docs/DESIGN.md index f89aa16d0b..1e8bfc381b 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -745,6 +745,22 @@ exact, while `int x = s[0];` must show that the element fits in an `int`. This is genuinely a CppVerify advantage over Verus — Verus forces users to maintain two separate bodies; we let one body do double duty *or* let users opt into a clean math-integer spec. +A lifted function's reference to a `const` integer, as a parameter or the +result, stands for the value it refers to, which it only reads: `constexpr +const T &larger(const T &a, const T &b)` is a spec of two values. One that +cannot be lifted (it reads memory through a pointer, or its type is not +supported) is kept as a declaration that uses an unsupported construct, so +the verdicts that rely on it are `Unresolved` with `construct.unsupported` +and name it. + +The standard library's functions are not lifted, since each library writes +them its own way and a verdict would depend on which one. `std::min` and +`std::max` of two integers, enumerations, or `bool` are modeled as the +standard defines them ([alg.min.max]): `max(a, b)` is `a < b ? b : a` and +`min(a, b)` is `b < a ? b : a`, read once each, in contracts and in code. +Any other function of the standard library that is not a constant is an +error naming it. + **Compile-time partial evaluation:** When a contract contains a `constexpr` call whose arguments are all constants, Clang evaluates it at compile time before the verifier sees it. A callee precondition instantiated at a call site is not such a call: there the argument is substituted for the parameter, and the solver settles the application from the lifted definition: @@ -1087,11 +1103,8 @@ immutable VCR address. A value use is a heap load, assignment is a heap store, and `cppverify::old(ref)` reads through the same address in the entry heap. Every reference receives a generated non-null and live entry precondition, -and its body is verified as reading the referent initialized. C++ does not -require that of an out-parameter, so a call that passes storage not yet -initialized (`int a; init(a);`) is `Unresolved` with reason -`construct.unsupported`, not a failure; so is a function that returns a -pointer to such storage. Distinct address parameters are object-range disjoint by default +and an initialized referent unless it is an out-parameter (below). +Distinct address parameters are object-range disjoint by default when at least one is mutable; `cppverify::aliases` permits the same complete object. `cppverify::modifies(ref)` is an open region rooted at the referent, matching `cppverify::modifies(*p)`. @@ -1105,6 +1118,54 @@ that pointer therefore does not rebind the reference. Binding reads nothing: a local reference may bind storage not yet initialized, and a read through it checks that the object is initialized. +#### Out-parameters + +Binding a reference or passing a pointer reads nothing ([dcl.init.ref], +[conv.lval]); only reading an indeterminate value is undefined +([basic.indet]). A function may therefore receive storage that is not +initialized yet, as long as it writes it before reading it, as C#'s `out` +parameters are definitely assigned before they are read. The contract +follows from the body, as `freshOwnedReturn` does, and the body is verified +against it: + +- **Which.** A pointer or reference parameter of a function with a verified + body (not a constructor's `this`, never assigned) is an out-parameter when + a walk of the body over every path finds each read of its storage at a + part (a byte offset from the parameter) written on every path before it, + the pointer used for nothing but accesses, null tests, validity, and calls + that pass it to another function's out-parameter, and no clause reading + the entry state reads the storage: preconditions (a class invariant + included), the measure, behaviors, `old`. A read at a computed offset, a + copy, or a callee that may read the storage (an input of a verified + callee, or any parameter of an external or trusted one) makes it an + input. Postconditions, loop invariants, and `cppverify::check` describe + what the body has written, so they are not reads for the walk, unless the + function never writes the storage: then they read the caller's values. + Recursion and calls between functions are settled by two fixpoints: the + parts each function writes on every path (least, so nothing rests on an + induction the walk does not do) and the out-parameters (greatest, so a + recursive call that passes the storage on reads nothing). +- **Contract.** The generated precondition asks for valid storage only. + Each part written on every path is a generated postcondition, + `initialized_ptr(p + offset)`, proved at the function's end as a + constructor's members are. +- **Body.** The storage's initialization is tracked as local storage's is: + a store initializes the part it writes, a loop that writes it starts each + iteration with what was initialized before it, and every read, those of + postconditions, invariants, and checks included, asserts `initialization`. + Its validity and frames stay those of any parameter. +- **Caller.** Where the argument is storage the caller tracks (a local, + dynamic storage, or its own out-parameter), the call keeps what was + initialized (initialization only grows), assumes the postconditions, the + generated ones included, and assumes the initialization each + postcondition's reads need, where it reads them: `cppverify::post(!result + || out == 5)` gives initialized storage where the result is true. + +A call that passes storage not yet initialized to an input is `Unresolved` +with reason `construct.unsupported`, not a failure, since the walk is +conservative; so is a function that returns a pointer to such storage, since +callers read a returned pointer's storage as initialized. + Only locals whose addresses are needed are spilled out of scalar SSA. Each such local becomes an automatic `VAllocateStmt` with a fresh lifetime identity, target size/alignment, byte ownership, liveness, and initialization metadata. @@ -1244,10 +1305,11 @@ void reset_left(Pair &p) again. - The generated validity clause of a reference or pointer parameter names its first byte; for a record the call also checks that its last byte lies - in the same live allocation (an allocation's bytes are contiguous) and that - every leaf is initialized, since the callee reads it as initialized storage. - An out-parameter, which C++ allows uninitialized, is - `construct.unsupported`, as for a scalar. + in the same live allocation (an allocation's bytes are contiguous) and, + unless the callee's parameter is an out-parameter, that every leaf is + initialized, since the callee may read it as initialized storage. A + caller's own out-parameter passed on to an input gets the same leaf + checks. - The callee's footprints inside the record are framed by their bytes (`HeapFrame`), a region as the whole record and never only its first cell; its writes need no footprint of the caller's, since the local is the @@ -1319,12 +1381,17 @@ void reset_left(Pair &p) - 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), + leaf and at its last byte (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. + name `this`. Its frame is `*this` and its own footprints, and `this` is + the object with its lifetime there, in the entry state too, so a member + function it calls writes inside the frame. A member function whose object + is an out-parameter may be called before the members are initialized; + one that may read them first may not (`construct.unsupported`). - 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 diff --git a/website/source/language/functions-loops.rst b/website/source/language/functions-loops.rst index 6137463e33..17fa5d2685 100644 --- a/website/source/language/functions-loops.rst +++ b/website/source/language/functions-loops.rst @@ -122,6 +122,50 @@ examined. Once a ``constexpr`` function has executable ``cppverify::pre``/``cppv clauses, it remains a modular executable function: calls must satisfy its preconditions and cannot be used as pure contract expressions. +A lifted function's parameter or result that is a reference to a ``const`` +integer stands for the value it refers to, as in ``constexpr const T +&larger(const T &a, const T &b)``. One that cannot be lifted (it reads memory +through a pointer, say) is reported, and a function that applies it is +``Unresolved`` with reason ``construct.unsupported``, naming it. + +The standard library's functions are not lifted: each library writes them +its own way, and a proof would depend on which one. ``std::min`` and +``std::max`` of two integers, enumerations, or ``bool`` mean what the +standard says they mean, in contracts and in code alike: ``std::max(a, b)`` +is ``a`` unless ``a < b``, and ``std::min(a, b)`` is ``a`` unless ``b < a``. + +.. code-block:: cpp + + #include + + int lower(int a, int b) + cv::post(cv::result == std::min(a, b)) + cv::post(cv::result <= a && cv::result <= b) + { + int m = std::min(a, b); + return m; + } + + long widened(int x) + cv::post(cv::result >= 3) + { + long w = std::max(x, 3L); + return w; + } + +.. code-block:: text + + Verified: lower [backend=z3] + Verified: widened [backend=z3] + +Any other function of the standard library, such as ``std::clamp``, is an +error naming it (``std::clamp is not modeled: of the standard library, the +verifier knows std::min and std::max of two integers``), as is a reference +bound to the result of ``std::max``. Before 0.2, ``std::min`` and +``std::max`` in a contract, and every ``constexpr`` helper that could not be +lifted, ended ``Unresolved: obligation lowering failed: f (missing spec +definition: fn_...)``. + Preconditions, ``cppverify::old(parameter)``, and a parameter named in a postcondition all denote the argument's entry value, as in ACSL, even when the callee reassigns its by-value parameter; a caller can therefore use the diff --git a/website/source/language/limitations.rst b/website/source/language/limitations.rst index 9c20cfa4a4..67786fe39b 100644 --- a/website/source/language/limitations.rst +++ b/website/source/language/limitations.rst @@ -284,8 +284,8 @@ Contracted executable free functions may accept ``T&`` and ``const T&`` when ``T`` is ``bool``, integral, or enum. VCR retains the binding as an immutable address: reading loads the referent, assignment stores through that address, and ``cppverify::old(ref)`` selects the entry heap. Every reference receives an implicit -non-null and live precondition, and the body is verified as reading the -referent initialized. +non-null and live precondition, and an initialized referent unless the body +writes it before reading it (an out-parameter, below). ``cppverify::modifies(ref)`` is an open region rooted at the referent, like ``cppverify::modifies(*p)``. Default object-range disjointness and ``cppverify::aliases`` apply across @@ -309,17 +309,22 @@ record. Conditional bindings, temporaries, reference returns, general raw address-taking/array decay (through such a reference too, and ``&x`` but as a call argument), and rvalue references remain fail-closed. A promoted object passed to a callee, by reference or ``&x``, keeps its lifetime: the callee -must keep no address of it, and every field must be initialized. Addressable declarations inside loops and ``cppverify::old`` of local +must keep no address of it, and every field must be initialized unless the +callee writes it before reading it. Addressable declarations inside loops and ``cppverify::old`` of local objects/bindings are also rejected; outer automatic locals and loop-local aliases are supported. Pointer leaves may retain abstract pointer values, but storing a provenance-bearing local dynamic pointer fails closed until pointer provenance is represented in a parallel heap. -A function is verified as reading its reference and pointer parameters' -storage, and its callers a returned pointer's, as initialized. C++ requires -neither, so a call that passes storage not yet initialized (an out-parameter, -``int a; init(a);``) and a function that returns a pointer to such storage are -``Unresolved`` with reason ``construct.unsupported``, not failures, until a -function can state that it writes a parameter before it reads it. A local +A reference or pointer parameter whose storage the body writes before it +reads it, an out-parameter, may receive storage not yet initialized +(``int a; init(a);``), as C++ allows (:doc:`pointers`). The rule is +syntactic: a read at a computed index (``p[i]``), a copy of the pointer, and +a callee that may read the storage first or has no verified body make the +parameter an input, and a call that passes storage not yet initialized to +an input is ``Unresolved`` with reason ``construct.unsupported``, not a +failure. Callers read a returned pointer's storage as initialized, so a +function that returns a pointer to storage not yet initialized is +``Unresolved`` the same way. A local reference may bind storage not yet initialized: a read through it checks that the object is initialized, as C++ does. Reference reads participate in the existing argument-order safety check. @@ -630,9 +635,11 @@ allocation from an archive. Libraries and real programs --------------------------- -CppVerify does not yet ship comprehensive libc or C++ standard-library models. -An uncontracted call fails closed; a contract is assumed only when it is -marked ``[[cppverify::trusted]]``. Contracts are not saved in precompiled +CppVerify does not yet ship comprehensive libc or C++ standard-library models: +of the standard library it knows ``std::min`` and ``std::max`` of two +integers (:doc:`functions-loops`), and any other of its functions is an +error naming it. An uncontracted call fails closed; a contract is assumed +only when it is marked ``[[cppverify::trusted]]``. Contracts are not saved in precompiled headers: a function declared in a PCH has no contract for the verifier, so a contracted function that calls it fails closed (``call to function without a verification contract``). diff --git a/website/source/language/pointers.rst b/website/source/language/pointers.rst index aec75e1722..5967193246 100644 --- a/website/source/language/pointers.rst +++ b/website/source/language/pointers.rst @@ -39,25 +39,52 @@ parameters for boolean, integral, and enum referents: The VCR parameter is an immutable address. Reading ``left`` loads the heap, assignment stores through the address, and ``cppverify::old(left)`` reads the entry heap. -CppVerify adds a non-null and live entry precondition for each reference, and -verifies the body as reading the referent initialized; a call that passes -storage not yet initialized is ``Unresolved`` (``construct.unsupported``). Mutable pointer/reference parameter pairs are object-range disjoint -by default (over whole ``valid(p, n)`` extents); -``cppverify::aliases(left, right)`` permits same-object aliasing. +CppVerify adds a non-null and live entry precondition for each reference, +and asks for initialized storage unless the function writes it before +reading it (an out-parameter, below). Mutable pointer/reference parameter +pairs are object-range disjoint by default (over whole ``valid(p, n)`` +extents); ``cppverify::aliases(left, right)`` permits same-object aliasing. Out-parameters ~~~~~~~~~~~~~~ -A function is verified as if it read its reference and pointer parameters' -storage, so every such parameter must refer to initialized storage at a call. -C++ requires less: a function that writes its parameter before reading it, -an out-parameter, may receive storage that is not initialized yet. Until a -contract can say that a function writes a parameter first, such a call is -``Unresolved`` with reason ``construct.unsupported``: neither proved nor -reported as a failure. - -.. cppverify-example: unresolved seven -.. cppverify-example: fails read_too_early +Binding a reference or passing a pointer reads nothing, so C++ lets a +function receive storage that is not initialized yet, provided it writes +the storage before it reads it. CppVerify finds such parameters in the +body. A pointer or reference parameter is an out-parameter when: + +- on every path, the body writes each part of the storage (the object, or + each field of a record) before it reads that part, through the parameter + itself; +- the body uses the pointer for nothing else than these accesses, a null + test, and passing it to another function's out-parameter: a copy of it, a + read at a computed index (``p[i]``), and a callee that may read the + storage first (or has no verified body) make it an input; +- its contract does not read the entry value: no precondition (a class + invariant of its record is one), measure, or ``cppverify::old`` reads the + storage, and if the function never writes it, no clause reads it at all. + +``--dump-ir=1`` prints ``param out out`` for each one. Its generated +precondition asks for valid storage only, and: + +- the function's reads of the storage, the reads of its postconditions, loop + invariants, and ``cppverify::check`` included, are checked against what it + has written (``initialization``); +- each part it writes on every path is initialized when it returns, a + generated postcondition ``initialized_ptr(p)`` (one per field of a + record): after a call the caller reads it as initialized, with the value + the postconditions give; +- where a postcondition reads a part, after a call it is initialized there + too, so a function that writes on some paths only, like ``try_get``, says + on which. + +Every other pointer or reference parameter needs initialized storage. A +call that passes storage not yet initialized to one is ``Unresolved`` with +reason ``construct.unsupported``: neither proved nor reported as a failure, +since the callee may read it first. + +.. cppverify-example: unresolved copied_garbage +.. cppverify-example: fails read_after_miss read_too_early .. code-block:: cpp @@ -68,6 +95,23 @@ reported as a failure. out = 7; } + bool try_get(int &out, bool ok) + cv::modifies(out) + cv::post(!cv::result || out == 5) + { + if (!ok) + return false; + out = 5; + return true; + } + + void copy_to(int &to, const int &from) + cv::modifies(to) + cv::post(to == from) + { + to = from; + } + int seven() cv::post(cv::result == 7) { @@ -76,14 +120,42 @@ reported as a failure. return a; } - int seven_initialized() + int five_or_zero(bool ok) + cv::post(cv::result == 5 || cv::result == 0) + { + int a; + bool found = try_get(a, ok); + if (found) + return a; + return 0; + } + + int read_after_miss() + cv::post(cv::result == 0) + { + int a; + try_get(a, false); + return a; + } + + int copied() cv::post(cv::result == 7) { - int a = 0; - init(a); + int a; + int b = 7; + copy_to(a, b); return a; } + int copied_garbage() + cv::post(cv::result == 0) + { + int a; + int b; + copy_to(a, b); + return 0; + } + int read_too_early() cv::post(cv::result == 3) { @@ -97,23 +169,37 @@ reported as a failure. .. code-block:: text Verified: init [backend=z3] - out.cpp:12:3: Unresolved: seven [backend=z3] [reason=construct.unsupported] (the verifier cannot model a construct here: binding a reference or pointer parameter to storage that is not initialized, since the callee is verified as reading initialized storage) - Verified: seven_initialized [backend=z3] - out.cpp:29:3: error: verification failed: read_too_early [...::initialization@29:3] (...) [backend=z3] [reason=counterexample] - -- Initializing the storage before the call, as ``seven_initialized`` does, is - the way to verify such code today. -- The same holds for an element of a local array (``init(arr[0])``), for - storage from ``new int`` passed to a pointer parameter before anything - writes it (``int *p = new int; init_ptr(p);``), and for a function that - returns a pointer to storage not initialized yet. + Verified: try_get [backend=z3] + Verified: copy_to [backend=z3] + Verified: seven [backend=z3] + Verified: five_or_zero [backend=z3] + out.cpp:48:3: error: verification failed: read_after_miss [...::initialization@48:3] (...) [backend=z3] [reason=counterexample] + Verified: copied [backend=z3] + out.cpp:65:3: Unresolved: copied_garbage [backend=z3] [reason=construct.unsupported] (the verifier cannot model a construct here: binding a reference or pointer parameter to storage that is not initialized, which the callee may read before writing it) + out.cpp:74:3: error: verification failed: read_too_early [...::initialization@74:3] (...) [backend=z3] [reason=counterexample] + +- ``copy_to``'s ``to`` is an out-parameter and ``from`` an input: + ``copied_garbage`` passes ``b`` uninitialized, which ``copy_to`` reads. +- ``try_get`` writes ``out`` on one path, so no generated postcondition + covers it; its own postcondition reads ``out`` where the result is true, + which is where ``five_or_zero`` reads it. After a miss, the read in + ``read_after_miss`` is a real error. +- The same holds for an element of a local array (``init(arr[0])``), + storage from ``new int`` (``int *p = new int; init_ptr(p);``), a record + written field by field (:doc:`structs`), and a member function that writes + its object before reading it (``Point p; p.reset();``), which a + constructor may also call before initializing its members. +- A function that returns a pointer to storage not initialized yet is still + ``Unresolved`` (``construct.unsupported``): its callers read the returned + storage as initialized. - A local reference may bind storage that is not initialized, as C++ allows, and a write through it initializes the object. A read before the first write is a real error, reported where it happens, as in ``read_too_early``. -Before 0.2 each of these calls was a reported failure (``verification failed: -... initialization``), and ``int a; init(a);`` stopped the whole file with -``error: seven: read of uninitialized local value: a``. +Before 0.2 each call that passed storage not yet initialized was a reported +failure (``verification failed: ... initialization``), and ``int a; +init(a);`` stopped the whole file with ``error: seven: read of uninitialized +local value: a``. Aliasing between parameters ~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/website/source/language/structs.rst b/website/source/language/structs.rst index 0418a15a4a..695fb75a9e 100644 --- a/website/source/language/structs.rst +++ b/website/source/language/structs.rst @@ -309,16 +309,17 @@ object. The call checks the rest: ``construct.unsupported`` (``the address of local or dynamic storage is passed to f, which may keep or free it, or has no verified body``); - the whole record lies in the live local; -- every field is initialized, since the callee reads its parameter's object - as initialized storage. C++ allows an out-parameter that is only written, - but the verifier does not model one yet: the call is ``Unresolved`` with - reason ``construct.unsupported``. +- every field is initialized when the callee may read its parameter's + object before writing it, else the call is ``Unresolved`` with reason + ``construct.unsupported``. A callee that writes each field it reads first + (an out-parameter, :doc:`pointers`) needs none of them initialized, and + the fields it writes on every path are initialized after the call. The callee then writes only its footprints inside the local, by their bytes, and every other local keeps its value. The caller's own ``cppverify::modifies`` need not name its locals. -.. cppverify-example: unresolved half_initialized +.. cppverify-example: unresolved no_limit .. code-block:: cpp @@ -368,21 +369,38 @@ and every other local keeps its value. The caller's own cv::post(cv::result == 1) { Counter c; - c.n = 0; set_n(c); return c.n; } + int limit_of(const Counter &c) + cv::post(cv::result == c.limit) + { + return c.limit; + } + + int no_limit() + cv::post(cv::result == 0) + { + Counter c; + c.n = 0; + int l = limit_of(c); + return 0; + } + .. code-block:: text Verified: bump [backend=z3] Verified: reset [backend=z3] Verified: set_n [backend=z3] Verified: counted [backend=z3] - counter.cpp:48:3: Unresolved: half_initialized [backend=z3] [reason=construct.unsupported] (the verifier cannot model a construct here: binding a reference or pointer parameter to storage that is not initialized, since the callee is verified as reading initialized storage) + Verified: half_initialized [backend=z3] + Verified: limit_of [backend=z3] + counter.cpp:62:3: Unresolved: no_limit [backend=z3] [reason=construct.unsupported] (the verifier cannot model a construct here: binding a reference or pointer parameter to storage that is not initialized, which the callee may read before writing it) -``half_initialized`` leaves ``c.limit`` uninitialized, and ``set_n`` would -read it as initialized. +``set_n`` writes ``c.n`` before reading it, so ``half_initialized`` may +leave ``c.limit`` uninitialized; ``limit_of`` reads ``c.limit``, which +``no_limit`` never initializes. The address of a local is supported as a call argument only. Stored in a pointer variable (``Counter *q = &c;``), or formed through a local reference @@ -715,8 +733,11 @@ array initialized (:doc:`functions-loops`). 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. + initialized needs initialized members only if it may read them before + writing them: one that writes them first (its object is an out-parameter, + :doc:`pointers`) may be called there, and the members it writes on every + path are initialized after the call. Calling one that may read them first + is ``construct.unsupported``. - 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, diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index 9ba26d6df8..6305f93b5f 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -173,9 +173,15 @@ was rejected as arithmetic on the pointer; values read through such a pointer are now ordinary integers (:doc:`language/dynamic-storage`). **Out-parameters.** Passing storage that is not initialized yet to a function -that writes it (``int a; init(a);``) was a failure, or stopped the file; it is -now ``Unresolved`` with reason ``construct.unsupported``, until a contract can -say that a function writes its parameter first (:doc:`language/pointers`). +that writes it (``int a; init(a);``) was a failure, or stopped the file. A +reference or pointer parameter whose storage the body writes before it reads +it is now an out-parameter: callers may pass storage not yet initialized, +the function's reads of it are checked against what it wrote, and the parts +it writes on every path, and those its postconditions read, are initialized +after a call. A call that passes such storage to a parameter the callee may +read first is ``Unresolved`` with reason ``construct.unsupported`` +(:doc:`language/pointers`). A constructor that calls a member function +writing its object no longer fails its frame check. **One condition, one choice.** Every ``cv::choose`` was a choice of its own, so ``cv::choose(k, k > n) == cv::choose(k, k > n)`` failed with a counterexample, @@ -348,6 +354,15 @@ that nothing instantiates is reported. ``cv::post(cv::result > 0)`` and ``cv::ol of a template's type did not compile (``invalid operands to binary expression ('T' and 'int')``) (:doc:`language/functions-loops`). +**std::min and std::max.** In a contract they ended ``Unresolved: +obligation lowering failed: f (missing spec definition: fn_...)``, as did +any function using a ``constexpr`` helper that could not be lifted. Of two +integers they now mean what the standard says, whatever the library, in +contracts and in code; any other function of the standard library is an +error naming it, a helper that cannot be lifted is named in the verdicts +that rely on it, and a lifted helper's references to ``const`` integers +stand for their values (:doc:`language/functions-loops`). + **Member operators.** For a member ``operator==``, ``a == b`` passed ``a`` for the operator's parameter and ``b`` as an argument beyond it, an error, and an operator returning ``*this`` by reference (``Money &operator+=``) was